Theorem map_incl_in_prod

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
03. 1 ⊢ function f, conj_elimll 2.
04. 1 ⊢ relation f, fn_is_rel 3.
05. 1 ⊢ dom f = X, conj_elimlr 2.
06. 1 ⊢ dom f ⊆ X, incl_from_eq 5.
07. 1 ⊢ rng f ⊆ Y, conj_elimr 2.
08. 1 ⊢ f ⊆ X × Y, relation_incl_prod 4 6 7.
map_incl_in_prod. ⊢ map f X Y → f ⊆ X × Y, subj_intro 8.

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