Proof
01. 1 ⊢ (a, c) ∈ S ∘ R, hypo.
02. ⊢ S ∘ R = {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
composition_eq.
03. 1 ⊢ (a, c) ∈ {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
eq_subst 2 1, P u ↔ (a, c) ∈ u.
04. 1 ⊢ ∃x. ∃y. ∃z. (a, c) = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S,
comp_elim 3.
05. 5 ⊢ ∃y. ∃z. (a, c) = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
06. 6 ⊢ ∃z. (a, c) = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
07. 7 ⊢ (a, c) = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
08. 7 ⊢ (a, c) = (x, z), conj_elimll 7.
09. 1 ⊢ set (a, c), set_intro 1.
10. 1 ⊢ set a, setl_from_pair 9.
11. 1 ⊢ set c, setr_from_pair 9.
12. 1, 7 ⊢ a = x ∧ c = z, pair_property 10 11 8.
13. 1, 7 ⊢ a = x, conj_eliml 12.
14. 1, 7 ⊢ c = z, conj_elimr 12.
15. 7 ⊢ (x, y) ∈ R, conj_elimlr 7.
16. 1, 7 ⊢ (a, y) ∈ R, eq_subst_rev 13 15.
17. 1, 7 ⊢ ∃y. (a, y) ∈ R, ex_intro 16.
18. 1, 6 ⊢ ∃y. (a, y) ∈ R, ex_elim 6 17.
19. 1, 5 ⊢ ∃y. (a, y) ∈ R, ex_elim 5 18.
20. 1 ⊢ ∃y. (a, y) ∈ R, ex_elim 4 19.
composition_elimr. ⊢ (a, c) ∈ S ∘ R → ∃y. (a, y) ∈ R, subj_intro 20.
21. 7 ⊢ (y, z) ∈ S, conj_elimr 7.
22. 1, 7 ⊢ (y, c) ∈ S, eq_subst_rev 14 21.
23. 1, 7 ⊢ ∃y. (y, c) ∈ S, ex_intro 22.
24. 1, 6 ⊢ ∃y. (y, c) ∈ S, ex_elim 6 23.
25. 1, 5 ⊢ ∃y. (y, c) ∈ S, ex_elim 5 24.
26. 1 ⊢ ∃y. (y, c) ∈ S, ex_elim 4 25.
composition_eliml. ⊢ (a, c) ∈ S ∘ R → ∃y. (y, c) ∈ S, subj_intro 26.
27. 1, 7 ⊢ (a, y) ∈ R ∧ (y, c) ∈ S, conj_intro 16 22.
28. 1, 7 ⊢ ∃y. (a, y) ∈ R ∧ (y, c) ∈ S, ex_intro 27.
29. 1, 6 ⊢ ∃y. (a, y) ∈ R ∧ (y, c) ∈ S, ex_elim 6 28.
30. 1, 5 ⊢ ∃y. (a, y) ∈ R ∧ (y, c) ∈ S, ex_elim 5 29.
31. 1 ⊢ ∃y. (a, y) ∈ R ∧ (y, c) ∈ S, ex_elim 4 30.
composition_elim. ⊢ (a, c) ∈ S ∘ R → ∃y. (a, y) ∈ R ∧ (y, c) ∈ S,
subj_intro 31.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.