map_rng

Theorem map_rng

Theorem. map_rng
map f X Y → rng f ⊆ Y

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
03. 1 ⊢ rng f ⊆ Y, conj_elimr 2.
map_rng. ⊢ map f X Y → rng f ⊆ Y, subj_intro 3.