let V be non empty set ; :: thesis: for f being Morphism of (Ens V) holds
( f is monic iff (@ f) `2 is one-to-one )
let f be Morphism of (Ens V); :: thesis: ( f is monic iff (@ f) `2 is one-to-one )
set m = @ f;
thus ( f is monic implies (@ f) `2 is one-to-one ) :: thesis: ( (@ f) `2 is one-to-one implies f is monic )

proof

assume A1: f is monic ; :: thesis: (@ f) `2 is one-to-one
set A = dom ((@ f) `2 );
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( 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
A2: ( x1 in dom ((@ f) `2 ) & x2 in dom ((@ f) `2 ) ) and
A3: ((@ f) `2 ) . x1 = ((@ f) `2 ) . x2 ; :: thesis: x1 = x2
A4: dom ((@ f) `2 ) = dom (@ f) by Lm3;
then reconsider A = dom ((@ f) `2 ) as Element of V ;
reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A2, FUNCOP_1:57;
reconsider m1 = [[A,A],fx1], m2 = [[A,A],fx2] as Element of Maps V by Th5;
set f1 = @ m1;
set f2 = @ m2;
A5: ( m1 = [[(dom m1),(cod m1)],(m1 `2 )] & m2 = [[(dom m2),(cod m2)],(m2 `2 )] ) by Th8;
then A6: ( dom m1 = A & dom m2 = A & cod m1 = A & cod m2 = A ) by Lm1;
( dom (@ (@ m1)) = A & dom (@ (@ m2)) = A & cod (@ (@ m1)) = A & cod (@ (@ m2)) = A ) by A5, Lm1;
then A7: ( dom (@ m1) = A & dom (@ m2) = A & cod (@ m1) = A & cod (@ m2) = A & dom f = A ) by A4, Def10, Def11;
set h1 = ((@ f) `2 ) * ((@ (@ m1)) `2 );
set h2 = ((@ f) `2 ) * ((@ (@ m2)) `2 );
set ff1 = (@ f) * (@ (@ m1));
set ff2 = (@ f) * (@ (@ m2));

now

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

now

thus A9: ( dom (((@ f) `2 ) * ((@ (@ m1)) `2 )) = A & dom (((@ f) `2 ) * ((@ (@ m2)) `2 )) = A ) by A6, A8, Lm3; :: thesis: for x being set st x in A holds
(((@ f) `2 ) * ((@ (@ m1)) `2 )) . x = (((@ f) `2 ) * ((@ (@ m2)) `2 )) . x
let x be set ; :: thesis: ( x in A implies (((@ f) `2 ) * ((@ (@ m1)) `2 )) . x = (((@ f) `2 ) * ((@ (@ m2)) `2 )) . x )
assume A10: x in A ; :: thesis: (((@ f) `2 ) * ((@ (@ m1)) `2 )) . x = (((@ f) `2 ) * ((@ (@ m2)) `2 )) . x
( fx1 = m1 `2 & fx2 = m2 `2 ) by A5, ZFMISC_1:33;
then ( ((@ (@ m1)) `2 ) . x = x1 & ((@ (@ m2)) `2 ) . x = x2 ) by A10, FUNCOP_1:13;
then ( (((@ f) `2 ) * ((@ (@ m1)) `2 )) . x = ((@ f) `2 ) . x1 & (((@ f) `2 ) * ((@ (@ m2)) `2 )) . x = ((@ f) `2 ) . x2 ) by A9, A10, FUNCT_1:22;
hence (((@ f) `2 ) * ((@ (@ m1)) `2 )) . x = (((@ f) `2 ) * ((@ (@ m2)) `2 )) . x by A3; :: thesis: verum

end;

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

end;

then ( (@ f) * (@ (@ m1)) = (@ f) * (@ (@ m2)) & f * (@ m1) = (@ f) * (@ (@ m1)) & f * (@ m2) = (@ f) * (@ (@ m2)) ) by A6, A7, Th28;
then ( @ m1 = @ m2 & @ m1 = m1 & @ m2 = m2 ) by A1, A7, CAT_1:def 10;
then fx1 = fx2 by ZFMISC_1:33;
hence x1 = fx2 . x1 by A2, FUNCOP_1:13
.= x2 by A2, FUNCOP_1:13 ;
:: thesis: verum

end;

assume A11: (@ f) `2 is one-to-one ; :: thesis: f is monic
let f1 be Morphism of (Ens V); :: according to CAT_1:def 10 :: thesis: for b<sub>1</sub> being Element of the carrier' of (Ens V) holds
( not dom f1 = dom b<sub>1</sub> or not cod f1 = dom f or not cod b<sub>1</sub> = dom f or not f * f1 = f * b<sub>1</sub> or f1 = b<sub>1</sub> )
let f2 be Morphism of (Ens V); :: thesis: ( not dom f1 = dom f2 or not cod f1 = dom f or not cod f2 = dom f or not f * f1 = f * f2 or f1 = f2 )
assume that
A12: dom f1 = dom f2 and
A13: ( cod f1 = dom f & cod f2 = dom f ) and
A14: f * f1 = f * f2 ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A15: ( dom (@ f1) = dom f1 & dom (@ f2) = dom f2 & cod (@ f1) = cod f1 & cod (@ f2) = cod f2 & dom (@ f) = dom f ) by Def10, Def11;
then ( (@ f) * (@ f1) = f * f1 & (@ f) * (@ f2) = f * f2 & (@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2 ) * ((@ f1) `2 ))] & (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2 ) * ((@ f2) `2 ))] ) by A13, Def7, Th28;
then ( dom ((@ f1) `2 ) = dom f1 & dom ((@ f2) `2 ) = dom f2 & dom ((@ f) `2 ) = dom f & rng ((@ f1) `2 ) c= cod f1 & rng ((@ f2) `2 ) c= cod f2 & ((@ f) `2 ) * ((@ f1) `2 ) = ((@ f) `2 ) * ((@ f2) `2 ) ) by A14, A15, Lm3, ZFMISC_1:33;
then ( (@ f1) `2 = (@ f2) `2 & @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2 )] & @ f2 = [[(dom (@ f2)),(cod (@ f2))],((@ f2) `2 )] ) by A11, A12, A13, Th8, FUNCT_1:49;
hence f1 = f2 by A12, A13, A15; :: thesis: verum