dom_incl

Theorem dom_incl

Theorem. dom_incl
R ⊆ X × Y → dom R ⊆ X

Proof
01. 1 ⊢ R ⊆ X × Y, hypo.
02. 2 ⊢ x ∈ dom R, hypo.
03. 2 ⊢ ∃y. (x, y) ∈ R, dom_elim 2.
04. 4 ⊢ (x, y) ∈ R, hypo.
05. 1, 4 ⊢ (x, y) ∈ X × Y, incl_elim 1 4.
06. 1, 4 ⊢ x ∈ X ∧ y ∈ Y, prod_elim_pair 5.
07. 1, 4 ⊢ x ∈ X, conj_eliml 6.
08. 1, 2 ⊢ x ∈ X, ex_elim 3 7.
09. 1 ⊢ x ∈ dom R → x ∈ X, subj_intro 8.
10. 1 ⊢ ∀x. x ∈ dom R → x ∈ X, uq_intro 9.
11. 1 ⊢ dom R ⊆ X, incl_intro 10.
dom_incl. ⊢ R ⊆ X × Y → dom R ⊆ X, subj_intro 11.

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