let V be non empty set ; :: thesis: for f being Morphism of (Ens V) st f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) holds
@ f is surjective
let f be Morphism of (Ens V); :: thesis: ( f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) implies @ f is surjective )
assume A1: f is epi ; :: thesis: ( for A being Element of V
for x1, x2 being set holds
( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )
given B being Element of V, x1, x2 being set such that A2: ( x1 in B & x2 in B ) and
A3: x1 <> x2 ; :: thesis: @ f is surjective
A4: rng ((@ f) `2 ) c= cod (@ f) by Lm3;
cod (@ f) c= rng ((@ f) `2 )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in cod (@ f) or x in rng ((@ f) `2 ) )
set A = cod (@ f);
assume that
A5: x in cod (@ f) and
A6: not x in rng ((@ f) `2 ) ; :: thesis: contradiction
reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A2, FUNCOP_1:57;
set h = {x} --> x2;
set g2 = g1 +* ({x} --> x2);
A7: x in {x} by TARSKI:def 1;
A8: ( dom g1 = cod (@ f) & dom ({x} --> x2) = {x} ) by FUNCOP_1:19;
then A9: dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by FUNCT_4:def 1
.= cod (@ f) by A5, ZFMISC_1:46 ;
( rng g1 = {x1} & rng ({x} --> x2) = {x2} ) by A5, FUNCOP_1:14;
then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by FUNCT_4:18;
then ( rng (g1 +* ({x} --> x2)) c= {x1,x2} & {x1,x2} c= B ) by A2, ENUMSET1:41, ZFMISC_1:38;
then rng (g1 +* ({x} --> x2)) c= B by XBOOLE_1:1;
then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A2, A9, FUNCT_2:def 1, RELSET_1:11;
reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A2, Th5;
set f1 = @ m1;
set f2 = @ m2;
A10: ( m1 = [[(dom m1),(cod m1)],(m1 `2 )] & m2 = [[(dom m2),(cod m2)],(m2 `2 )] ) by Th8;
then A11: ( dom m1 = cod (@ f) & dom m2 = cod (@ f) & cod m1 = B & cod m2 = B ) by Lm1;
( dom (@ (@ m1)) = cod (@ f) & dom (@ (@ m2)) = cod (@ f) & cod (@ (@ m1)) = B & cod (@ (@ m2)) = B ) by A10, Lm1;
then A12: ( dom (@ m1) = cod (@ f) & dom (@ m2) = cod (@ f) & cod (@ m1) = B & cod (@ m2) = B & cod f = cod (@ f) ) by Def10, Def11;
A13: ( g1 = m1 `2 & g2 = m2 `2 ) by A10, ZFMISC_1:33;
set h1 = ((@ (@ m1)) `2 ) * ((@ f) `2 );
set h2 = ((@ (@ m2)) `2 ) * ((@ f) `2 );
set f1f = (@ (@ m1)) * (@ f);
set f2f = (@ (@ m2)) * (@ f);

now

A14: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2 ) * ((@ f) `2 ) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) & cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) & ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2 ) * ((@ f) `2 ) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) & cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) ) by A11, Th12;
hence ( (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2 ) * ((@ f) `2 ))] & (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2 ) * ((@ f) `2 ))] ) by Th8; :: thesis: ((@ (@ m1)) `2 ) * ((@ f) `2 ) = ((@ (@ m2)) `2 ) * ((@ f) `2 )

now

thus A15: ( dom (((@ (@ m1)) `2 ) * ((@ f) `2 )) = dom (@ f) & dom (((@ (@ m2)) `2 ) * ((@ f) `2 )) = dom (@ f) ) by A14, Lm3; :: thesis: for z being set st z in dom (@ f) holds
(((@ (@ m1)) `2 ) * ((@ f) `2 )) . z = (((@ (@ m2)) `2 ) * ((@ f) `2 )) . z
let z be set ; :: thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2 ) * ((@ f) `2 )) . z = (((@ (@ m2)) `2 ) * ((@ f) `2 )) . z )
set y = ((@ f) `2 ) . z;
assume A16: z in dom (@ f) ; :: thesis: (((@ (@ m1)) `2 ) * ((@ f) `2 )) . z = (((@ (@ m2)) `2 ) * ((@ f) `2 )) . z
then z in dom ((@ f) `2 ) by Lm3;
then ((@ f) `2 ) . z in rng ((@ f) `2 ) by FUNCT_1:def 5;
then ( (((@ (@ m1)) `2 ) * ((@ f) `2 )) . z = g1 . (((@ f) `2 ) . z) & (((@ (@ m2)) `2 ) * ((@ f) `2 )) . z = g2 . (((@ f) `2 ) . z) & not ((@ f) `2 ) . z in {x} & g1 . (((@ f) `2 ) . z) = x1 ) by A4, A6, A13, A15, A16, FUNCOP_1:13, FUNCT_1:22, TARSKI:def 1;
hence (((@ (@ m1)) `2 ) * ((@ f) `2 )) . z = (((@ (@ m2)) `2 ) * ((@ f) `2 )) . z by A8, FUNCT_4:12; :: thesis: verum

end;

hence ((@ (@ m1)) `2 ) * ((@ f) `2 ) = ((@ (@ m2)) `2 ) * ((@ f) `2 ) by FUNCT_1:9; :: thesis: verum

end;

then ( (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) & (@ m1) * f = (@ (@ m1)) * (@ f) & (@ m2) * f = (@ (@ m2)) * (@ f) & ({x} --> x2) . x = x2 ) by A7, A11, A12, Th28, FUNCOP_1:13;
then ( @ m1 = @ m2 & g1 . x = x1 & g2 . x = x2 ) by A1, A5, A7, A8, A12, CAT_1:def 11, FUNCOP_1:13, FUNCT_4:14;
hence contradiction by A3, ZFMISC_1:33; :: thesis: verum

end;

hence rng ((@ f) `2 ) = cod (@ f) by A4, XBOOLE_0:def 10; :: according to ENS_1:def 9 :: thesis: verum