map_rng_weaken

Theorem map_rng_weaken

Theorem. map_rng_weaken
map f X Y → Y ⊆ Z → map f X Z

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ Y ⊆ Z, hypo.
03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
04. 1 ⊢ function f, conj_elimll 3.
05. 1 ⊢ dom f = X, conj_elimlr 3.
06. 1 ⊢ rng f ⊆ Y, conj_elimr 3.
07. 1, 2 ⊢ rng f ⊆ Z, incl_trans 6 2.
08. 1, 2 ⊢ map f X Z, map_intro 4 5 7.
map_rng_weaken. ⊢ map f X Y → Y ⊆ Z → map f X Z, subj_intro_ii 8.