Proof
01. 1 ⊢ (a, b) ∈ R, hypo.
02. 2 ⊢ (b, c) ∈ S, hypo.
03. ⊢ (a, c) = (a, c), eq_refl.
04. 1 ⊢ (a, c) = (a, c) ∧ (a, b) ∈ R, conj_intro 3 1.
05. 1, 2 ⊢ (a, c) = (a, c) ∧ (a, b) ∈ R ∧ (b, c) ∈ S, conj_intro 4 2.
06. 1, 2 ⊢ ∃z. (a, c) = (a, z) ∧ (a, b) ∈ R ∧ (b, z) ∈ S, ex_intro 5.
07. 1, 2 ⊢ ∃y. ∃z. (a, c) = (a, z) ∧ (a, y) ∈ R ∧ (y, z) ∈ S, ex_intro 6.
08. 1, 2 ⊢ ∃x. ∃y. ∃z. (a, c) = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S, ex_intro 7.
09. 1 ⊢ set (a, b), set_intro 1.
10. 2 ⊢ set (b, c), set_intro 2.
11. 1 ⊢ set a, setl_from_pair 9.
12. 2 ⊢ set c, setr_from_pair 10.
13. 1, 2 ⊢ set (a, c), set_pair 11 12.
14. 1, 2 ⊢ (a, c) ∈ {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
comp_intro 13 8, P t ↔ (∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S).
15. ⊢ S ∘ R = {t | ∃x. ∃y. ∃z. t = (x, z) ∧ (x, y) ∈ R ∧ (y, z) ∈ S},
composition_eq.
16. 1, 2 ⊢ (a, c) ∈ S ∘ R, eq_subst_rev 15 14, P u ↔ (a, c) ∈ u.
composition_intro. ⊢ (a, b) ∈ R → (b, c) ∈ S → (a, c) ∈ S ∘ R,
subj_intro_ii 16.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.