let X be non empty set ; :: thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let o1, o2 be object of (EnsCat X); :: thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one ) )
assume A1: <^o1,o2^> <> {} ; :: thesis: for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let A be Morphism of o1,o2; :: thesis: for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
let F be Function of o1,o2; :: thesis: ( F = A implies ( A is mono iff F is one-to-one ) )
assume A2: F = A ; :: thesis: ( A is mono iff F is one-to-one )
per cases ( o2 <> {} or o2 = {} ) ;
suppose o2 <> {} ; :: thesis: ( A is mono iff F is one-to-one )
then A3: dom F = o1 by FUNCT_2:def 1;
thus ( A is mono implies F is one-to-one ) :: thesis: ( F is one-to-one implies A is mono )
proof
assume A4: A is mono ; :: thesis: F is one-to-one
assume not F is one-to-one ; :: thesis: contradiction
then consider x1, x2 being set such that
A5: ( x1 in dom F & x2 in dom F ) and
A6: F . x1 = F . x2 and
A7: x1 <> x2 by FUNCT_1:def 8;
set o = o1;
A8: <^o1,o1^> <> {} by ALTCAT_1:23;
set B = o1 --> x1;
A9: dom (o1 --> x1) = o1 by FUNCOP_1:19;
set C = o1 --> x2;
A10: dom (o1 --> x2) = o1 by FUNCOP_1:19;
consider o' being Element of o1;
(o1 --> x1) . o' = x1 by A3, A5, FUNCOP_1:13;
then A11: (o1 --> x1) . o' <> (o1 --> x2) . o' by A3, A5, A7, FUNCOP_1:13;
A12: rng (o1 --> x1) c= o1
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o1 --> x1) or y in o1 )
assume y in rng (o1 --> x1) ; :: thesis: y in o1
then consider x being set such that
A13: ( x in dom (o1 --> x1) & (o1 --> x1) . x = y ) by FUNCT_1:def 5;
thus y in o1 by A3, A5, A9, A13, FUNCOP_1:13; :: thesis: verum
end;
then o1 --> x1 in Funcs o1,o1 by A9, FUNCT_2:def 2;
then reconsider B1 = o1 --> x1 as Morphism of o1,o1 by ALTCAT_1:def 16;
A14: rng (o1 --> x2) c= o1
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o1 --> x2) or y in o1 )
assume y in rng (o1 --> x2) ; :: thesis: y in o1
then consider x being set such that
A15: ( x in dom (o1 --> x2) & (o1 --> x2) . x = y ) by FUNCT_1:def 5;
thus y in o1 by A3, A5, A10, A15, FUNCOP_1:13; :: thesis: verum
end;
then o1 --> x2 in Funcs o1,o1 by A10, FUNCT_2:def 2;
then reconsider C1 = o1 --> x2 as Morphism of o1,o1 by ALTCAT_1:def 16;
A16: dom (F * (o1 --> x1)) = o1 by A3, A9, A12, RELAT_1:46;
A17: dom (F * (o1 --> x2)) = o1 by A3, A10, A14, RELAT_1:46;
now
let z be set ; :: thesis: ( z in o1 implies (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z )
assume A18: z in o1 ; :: thesis: (F * (o1 --> x1)) . z = (F * (o1 --> x2)) . z
hence (F * (o1 --> x1)) . z = F . ((o1 --> x1) . z) by A16, FUNCT_1:22
.= F . x2 by A6, A18, FUNCOP_1:13
.= F . ((o1 --> x2) . z) by A18, FUNCOP_1:13
.= (F * (o1 --> x2)) . z by A17, A18, FUNCT_1:22 ;
:: thesis: verum
end;
then F * (o1 --> x1) = F * (o1 --> x2) by A16, A17, FUNCT_1:9;
then A * B1 = F * (o1 --> x2) by A1, A2, A8, ALTCAT_1:18
.= A * C1 by A1, A2, A8, ALTCAT_1:18 ;
hence contradiction by A4, A8, A11, Def7; :: thesis: verum
end;
thus ( F is one-to-one implies A is mono ) :: thesis: verum
proof
assume A19: F is one-to-one ; :: thesis: A is mono
let o be object of (EnsCat X); :: according to ALTCAT_3:def 7 :: thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A20: <^o,o1^> <> {} ; :: thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; :: thesis: ( A * B = A * C implies B = C )
assume A21: A * B = A * C ; :: thesis: B = C
A22: <^o,o1^> = Funcs o,o1 by ALTCAT_1:def 16;
then consider B1 being Function such that
A23: ( B1 = B & dom B1 = o & rng B1 c= o1 ) by A20, FUNCT_2:def 2;
consider C1 being Function such that
A24: ( C1 = C & dom C1 = o & rng C1 c= o1 ) by A20, A22, FUNCT_2:def 2;
A25: <^o,o2^> <> {} by A1, A20, ALTCAT_1:def 4;
then A26: F * B1 = A * C by A1, A2, A20, A21, A23, ALTCAT_1:18
.= F * C1 by A1, A2, A20, A24, A25, ALTCAT_1:18 ;
now
let z be set ; :: thesis: ( z in o implies B1 . z = C1 . z )
assume A27: z in o ; :: thesis: B1 . z = C1 . z
then A28: ( B1 . z in rng B1 & C1 . z in rng C1 ) by A23, A24, FUNCT_1:def 5;
F . (B1 . z) = (F * B1) . z by A23, A27, FUNCT_1:23;
then F . (B1 . z) = F . (C1 . z) by A24, A26, A27, FUNCT_1:23;
hence B1 . z = C1 . z by A3, A19, A23, A24, A28, FUNCT_1:def 8; :: thesis: verum
end;
hence B = C by A23, A24, FUNCT_1:9; :: thesis: verum
end;
end;
suppose A29: o2 = {} ; :: thesis: ( A is mono iff F is one-to-one )
hence ( A is mono implies F is one-to-one ) ; :: thesis: ( F is one-to-one implies A is mono )
thus ( F is one-to-one implies A is mono ) :: thesis: verum
proof
assume F is one-to-one ; :: thesis: A is mono
let o be object of (EnsCat X); :: according to ALTCAT_3:def 7 :: thesis: ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A31: <^o,o1^> <> {} ; :: thesis: for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; :: thesis: ( A * B = A * C implies B = C )
assume A * B = A * C ; :: thesis: B = C
A32: <^o,o1^> = Funcs o,o1 by ALTCAT_1:def 16;
then consider B1 being Function such that
A33: ( B1 = B & dom B1 = o & rng B1 c= o1 ) by A31, FUNCT_2:def 2;
consider C1 being Function such that
A34: ( C1 = C & dom C1 = o & rng C1 c= o1 ) by A31, A32, FUNCT_2:def 2;
A35: <^o1,o2^> = Funcs o1,o2 by ALTCAT_1:def 16;
consider x being Element of Funcs o1,o2;
consider f being Function such that
A36: ( f = x & dom f = o1 & rng f c= o2 ) by A1, A35, FUNCT_2:def 2;
rng f = {} by A29, A36, XBOOLE_1:3;
then dom f = {} by RELAT_1:65;
then A37: rng B1 = {} by A33, A36, XBOOLE_1:3;
then A38: dom B1 = {} by RELAT_1:65;
B1 = {} by A37, RELAT_1:64
.= C1 by A33, A34, A38, RELAT_1:64 ;
hence B = C by A33, A34; :: thesis: verum
end;
end;
end;