fn_is_map

Theorem fn_is_map

Theorem. fn_is_map
function f → dom f = X → map f X UnivCl

Proof
01. 1 ⊢ function f, hypo.
02. 2 ⊢ dom f = X, hypo.
03. ⊢ rng f ⊆ UnivCl, UnivCl_is_greatest.
04. 1, 2 ⊢ map f X UnivCl, map_intro 1 2 3.
fn_is_map. ⊢ function f → dom f = X → map f X UnivCl, subj_intro_ii 4.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.