let V be non empty set ; 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); 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; ( 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) <> {}
; ( 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
; ( 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
; @ 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 ;
TARSKI:def 3 ( 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)
;
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;
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;
verum
end;
rng ((@ f) `2) c= cod (@ f)
by Lm3;
hence
rng ((@ f) `2) = cod (@ f)
by A6, XBOOLE_0:def 10; ENS_1:def 8 verum