sur_intro

Theorem sur_intro

Theorem. sur_intro
map f X Y → Y ⊆ rng f → sur f X Y

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ Y ⊆ rng f, hypo.
03. 1 ⊢ rng f ⊆ Y, lsubj_conj_elimr map_equi 1.
04. 1, 2 ⊢ rng f = Y, incl_antisym 3 2.
05. 1, 2 ⊢ map f X Y ∧ rng f = Y, conj_intro 1 4.
06. 1, 2 ⊢ sur f X Y, rsubj_elim sur_equi 5.
sur_intro. ⊢ map f X Y → Y ⊆ rng f → sur f X Y, subj_intro_ii 6.

Dependencies
The given proof depends on one axiom:
ext.