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) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
let a, b be Object of (Ens V); for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
let f be Morphism of a,b; ( Hom (a,b) <> {} implies ( f is monic iff (@ f) `2 is one-to-one ) )
assume A1:
Hom (a,b) <> {}
; ( f is monic iff (@ f) `2 is one-to-one )
set m = @ f;
A2:
dom (@ f) = dom f
by Def9;
then A3:
dom ((@ f) `2) = dom f
by Lm3;
thus
( f is monic implies (@ f) `2 is one-to-one )
( (@ f) `2 is one-to-one implies f is monic )proof
set A =
dom ((@ f) `2);
assume A4:
f is
monic
;
(@ f) `2 is one-to-one
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in proj1 ((@ f) `2) or not x2 in proj1 ((@ f) `2) or not ((@ f) `2) . x1 = ((@ f) `2) . x2 or x1 = x2 )
assume that A5:
x1 in dom ((@ f) `2)
and A6:
x2 in dom ((@ f) `2)
and A7:
((@ f) `2) . x1 = ((@ f) `2) . x2
;
x1 = x2
A8:
dom ((@ f) `2) = dom (@ f)
by Lm3;
then reconsider A =
dom ((@ f) `2) as
Element of
V ;
A9:
dom f = A
by A8, Def9;
reconsider fx1 =
A --> x1,
fx2 =
A --> x2 as
Function of
A,
A by A5, A6, FUNCOP_1:45;
reconsider m1 =
[[A,A],fx1],
m2 =
[[A,A],fx2] as
Element of
Maps V by Th5;
set f1 =
@ m1;
set f2 =
@ m2;
set h1 =
((@ f) `2) * ((@ (@ m1)) `2);
set h2 =
((@ f) `2) * ((@ (@ m2)) `2);
set ff1 =
(@ f) * (@ (@ m1));
set ff2 =
(@ f) * (@ (@ m2));
A10:
cod m2 = A
;
then A11:
(
((@ f) * (@ (@ m2))) `2 = ((@ f) `2) * ((@ (@ m2)) `2) &
dom ((@ f) * (@ (@ m2))) = dom (@ (@ m2)) )
by A8, Th12;
cod ((@ f) * (@ (@ m2))) = cod (@ f)
by A8, A10, Th12;
then A12:
(@ f) * (@ (@ m2)) = [[(dom (@ (@ m2))),(cod (@ f))],(((@ f) `2) * ((@ (@ m2)) `2))]
by A11, Th8;
dom (@ (@ m2)) = A
;
then A13:
dom (@ m2) = A
by Def9;
cod (@ (@ m2)) = A
;
then A14:
cod (@ m2) = A
by Def10;
then A15:
f (*) (@ m2) = (@ f) * (@ (@ m2))
by A9, Th27;
A16:
cod m1 = A
;
then A17:
(
((@ f) * (@ (@ m1))) `2 = ((@ f) `2) * ((@ (@ m1)) `2) &
dom ((@ f) * (@ (@ m1))) = dom (@ (@ m1)) )
by A8, Th12;
now ( dom (((@ f) `2) * ((@ (@ m1)) `2)) = A & dom (((@ f) `2) * ((@ (@ m2)) `2)) = A & ( for x being object st x in A holds
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x ) )thus A18:
(
dom (((@ f) `2) * ((@ (@ m1)) `2)) = A &
dom (((@ f) `2) * ((@ (@ m2)) `2)) = A )
by A17, A11, Lm3;
for x being object st x in A holds
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . xlet x be
object ;
( x in A implies (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x )assume A19:
x in A
;
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
((@ (@ m1)) `2) . x = x1
by A19, FUNCOP_1:7;
then A20:
(((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1
by A18, A19, FUNCT_1:12;
((@ (@ m2)) `2) . x = x2
by A19, FUNCOP_1:7;
hence
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
by A7, A18, A19, A20, FUNCT_1:12;
verum end;
then A21:
((@ f) `2) * ((@ (@ m1)) `2) = ((@ f) `2) * ((@ (@ m2)) `2)
;
cod ((@ f) * (@ (@ m1))) = cod (@ f)
by A8, A16, Th12;
then A22:
(@ f) * (@ (@ m1)) = [[(dom (@ (@ m1))),(cod (@ f))],(((@ f) `2) * ((@ (@ m1)) `2))]
by A17, Th8;
dom (@ (@ m1)) = A
;
then A23:
dom (@ m1) = A
by Def9;
cod (@ (@ m1)) = A
;
then A24:
cod (@ m1) = A
by Def10;
reconsider A =
A as
Object of
(Ens V) ;
A25:
dom f = a
by A1, CAT_1:5;
then A26:
(
@ m1 in Hom (
A,
a) &
@ m2 in Hom (
A,
a) )
by A23, A9, A24, A13, A14;
then reconsider f1 =
@ m1,
f2 =
@ m2 as
Morphism of
A,
a by CAT_1:def 5;
A27:
f * f1 =
f (*) f1
by A1, A26, CAT_1:def 13
.=
f (*) f2
by A22, A12, A21, A15, A24, A9, Th27
.=
f * f2
by A1, A26, CAT_1:def 13
;
Hom (
A,
a)
<> {}
by A25, A9;
then
f1 = f2
by A4, A27;
then
fx1 = fx2
by XTUPLE_0:1;
hence x1 =
fx2 . x1
by A5, FUNCOP_1:7
.=
x2
by A5, FUNCOP_1:7
;
verum
end;
assume A28:
(@ f) `2 is one-to-one
; f is monic
thus
Hom (a,b) <> {}
by A1; CAT_1:def 14 for b1 being Element of the carrier of (Ens V) holds
( Hom (b1,a) = {} or for b2, b3 being Morphism of b1,a holds
( not f * b2 = f * b3 or b2 = b3 ) )
let c be Object of (Ens V); ( Hom (c,a) = {} or for b1, b2 being Morphism of c,a holds
( not f * b1 = f * b2 or b1 = b2 ) )
assume A29:
Hom (c,a) <> {}
; for b1, b2 being Morphism of c,a holds
( not f * b1 = f * b2 or b1 = b2 )
let f1, f2 be Morphism of c,a; ( not f * f1 = f * f2 or f1 = f2 )
A30: dom f1 =
c
by A29, CAT_1:5
.=
dom f2
by A29, CAT_1:5
;
A31: cod f1 =
a
by A29, CAT_1:5
.=
dom f
by A1, CAT_1:5
;
A32: cod f2 =
a
by A29, CAT_1:5
.=
dom f
by A1, CAT_1:5
;
assume A33:
f * f1 = f * f2
; f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A34: (@ f) * (@ f1) =
f (*) f1
by A31, Th27
.=
f * f1
by A29, A1, CAT_1:def 13
;
A35: (@ f) * (@ f2) =
f (*) f2
by A32, Th27
.=
f * f2
by A29, A1, CAT_1:def 13
;
A36:
@ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)]
by Th8;
A37:
dom (@ f2) = dom f2
by Def9;
then A38:
dom ((@ f2) `2) = dom f2
by Lm3;
A39:
cod (@ f1) = cod f1
by Def10;
then A40:
rng ((@ f1) `2) c= cod f1
by Lm3;
A41:
cod (@ f2) = cod f2
by Def10;
then A42:
rng ((@ f2) `2) c= cod f2
by Lm3;
A43:
(@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))]
by A32, A41, A2, Def6;
(@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))]
by A31, A39, A2, Def6;
then A44:
((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2)
by A35, A33, A34, A43, XTUPLE_0:1;
A45:
dom (@ f1) = dom f1
by Def9;
then
dom ((@ f1) `2) = dom f1
by Lm3;
then
(@ f1) `2 = (@ f2) `2
by A28, A30, A31, A32, A38, A3, A40, A42, A44, FUNCT_1:27;
hence
f1 = f2
by A30, A31, A32, A45, A37, A39, A41, A36, Th8; verum