Proof 01. 1 ⊢ map f X Y, hypo. 02. 2 ⊢ A ⊆ X, hypo. 03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1. 04. 1 ⊢ function f ∧ dom f = X, conj_eliml 3. 05. 1 ⊢ function f, conj_eliml 4. 06. 1 ⊢ dom f = X, conj_elimr 4. 07. 1 ⊢ rng f ⊆ Y, conj_elimr 3. 08. ⊢ restr f A ⊆ f, restr_is_subclass. 09. 1 ⊢ function (restr f A), function_subclass 8 5. 10. 1, 2 ⊢ dom (restr f A) = A, dom_restr_subclass 1 2. 11. ⊢ rng (restr f A) ⊆ rng f, rng_subclass 8. 12. 1 ⊢ rng (restr f A) ⊆ Y, incl_trans 11 7. 13. 1, 2 ⊢ map (restr f A) A Y, map_intro 9 10 12. map_restr. ⊢ map f X Y → A ⊆ X → map (restr f A) A Y, subj_intro_ii 13.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.