let V be non empty set ; :: thesis: for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} & 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 a, b be Object of (Ens V); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & 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 a,b; :: thesis: ( Hom (a,b) <> {} & 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: Hom (a,b) <> {} ; :: thesis: ( not f is epi or 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 )
assume A2: 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 A3: x1 in B and
A4: x2 in B and
A5: x1 <> x2 ; :: thesis: @ f is surjective
A6: cod (@ f) c= rng ((@ f) `2)
proof
set A = cod (@ f);
reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A3, FUNCOP_1:45;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cod (@ f) or x in rng ((@ f) `2) )
assume that
A7: x in cod (@ f) and
A8: not x in rng ((@ f) `2) ; :: thesis: contradiction
set h = {x} --> x2;
set g2 = g1 +* ({x} --> x2);
A9: dom ({x} --> x2) = {x} by FUNCOP_1:13;
A10: rng ({x} --> x2) = {x2} by FUNCOP_1:8;
rng g1 = {x1} by A7, FUNCOP_1:8;
then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by A10, FUNCT_4:17;
then A11: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;
{x1,x2} c= B by A3, A4, ZFMISC_1:32;
then A12: rng (g1 +* ({x} --> x2)) c= B by A11;
dom g1 = cod (@ f) by FUNCOP_1:13;
then dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by A9, FUNCT_4:def 1
.= cod (@ f) by A7, ZFMISC_1:40 ;
then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A3, A12, FUNCT_2:def 1, RELSET_1:4;
A13: cod f = cod (@ f) by Def10;
A14: x in {x} by TARSKI:def 1;
then ({x} --> x2) . x = x2 by FUNCOP_1:7;
then A15: g2 . x = x2 by A14, A9, FUNCT_4:13;
A16: g1 . x = x1 by A7, FUNCOP_1:7;
reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A3, Th5;
set f1 = @ m1;
set f2 = @ m2;
set h1 = ((@ (@ m1)) `2) * ((@ f) `2);
set h2 = ((@ (@ m2)) `2) * ((@ f) `2);
set f1f = (@ (@ m1)) * (@ f);
set f2f = (@ (@ m2)) * (@ f);
A17: dom m1 = cod (@ f) ;
then A18: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2) * ((@ f) `2) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) ) by Th12;
A19: dom m2 = cod (@ f) ;
then A20: ( ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2) * ((@ f) `2) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) ) by Th12;
cod (@ (@ m2)) = B ;
then A21: cod (@ m2) = B by Def10;
dom (@ (@ m2)) = cod (@ f) ;
then A22: dom (@ m2) = cod (@ f) by Def9;
then A23: (@ m2) (*) f = (@ (@ m2)) * (@ f) by A13, Th27;
now :: thesis: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) & ( for z being object st z in dom (@ f) holds
(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z ) )
thus A24: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) ) by A18, A20, Lm3; :: thesis: for z being object st z in dom (@ f) holds
(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z
let z be object ; :: thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z )
set y = ((@ f) `2) . z;
assume A25: 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 3;
then A26: not ((@ f) `2) . z in {x} by A8, TARSKI:def 1;
( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by A24, A25, FUNCT_1:12;
hence (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by A9, A26, FUNCT_4:11; :: thesis: verum
end;
then A27: ((@ (@ m1)) `2) * ((@ f) `2) = ((@ (@ m2)) `2) * ((@ f) `2) ;
cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by A17, Th12;
then A28: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by A18, Th8;
cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by A19, Th12;
then A29: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by A20, Th8;
A30: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by A28, A29, A27;
cod (@ (@ m1)) = B ;
then A31: cod (@ m1) = B by Def10;
dom (@ (@ m1)) = cod (@ f) ;
then A32: dom (@ m1) = cod (@ f) by Def9;
reconsider B = B as Object of (Ens V) ;
A33: cod f = b by A1, CAT_1:5;
then A34: @ m1 in Hom (b,B) by A13, A31, A32;
then reconsider f1 = @ m1 as Morphism of b,B by CAT_1:def 5;
@ m2 in Hom (b,B) by A13, A21, A22, A33;
then reconsider f2 = @ m2 as Morphism of b,B by CAT_1:def 5;
f1 * f = f1 (*) f by A1, A34, CAT_1:def 13
.= f2 (*) f by A30, A23, A32, A13, Th27
.= f2 * f by A1, A34, CAT_1:def 13 ;
then f1 = f2 by A2, A34;
hence contradiction by A5, A16, A15, XTUPLE_0:1; :: thesis: verum
end;
rng ((@ f) `2) c= cod (@ f) by Lm3;
hence rng ((@ f) `2) = cod (@ f) by A6, XBOOLE_0:def 10; :: according to ENS_1:def 8 :: thesis: verum