dom_composition

Theorem dom_composition

Theorem. dom_composition
dom (S ∘ R) ⊆ dom R

Proof
01. 1 ⊢ x ∈ dom (S ∘ R), hypo.
02. 1 ⊢ ∃z. (x, z) ∈ S ∘ R, dom_elim 1.
03. 3 ⊢ (x, z) ∈ S ∘ R, hypo.
04. 3 ⊢ ∃y. (x, y) ∈ R, composition_elimr 3.
05. 5 ⊢ (x, y) ∈ R, hypo.
06. 5 ⊢ x ∈ dom R, dom_intro 5.
07. 3 ⊢ x ∈ dom R, ex_elim 4 6.
08. 1 ⊢ x ∈ dom R, ex_elim 2 7.
09. ⊢ x ∈ dom (S ∘ R) → x ∈ dom R, subj_intro 8.
10. ⊢ ∀x. x ∈ dom (S ∘ R) → x ∈ dom R, uq_intro 9.
dom_composition. ⊢ dom (S ∘ R) ⊆ dom R, incl_intro 10.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.