map_intro

Theorem map_intro

Theorem. map_intro
function f → dom f = X → rng f ⊆ Y → map f X Y

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ dom f = X, hypo.
03. 3 ⊢ rng f ⊆ Y, hypo.
04. 1, 2 ⊢ function f ∧ dom f = X, conj_intro 1 2.
05. 1, 2, 3 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, conj_intro 4 3.
06. ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y → map f X Y, bij_elimr map_equi.
07. 1, 2, 3 ⊢ map f X Y, subj_elim 6 5.
map_intro. ⊢ function f → dom f = X → rng f ⊆ Y → map f X Y,
  subj_intro_iii 7.