let X be non empty set ; 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); ( <^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^> <> {}
; 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; 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; ( F = A implies ( A is mono iff F is one-to-one ) )
assume A2:
F = A
; ( A is mono iff F is one-to-one )
per cases
( o2 <> {} or o2 = {} )
;
suppose
o2 <> {}
;
( 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 )
( F is one-to-one implies A is mono )proof
set o =
o1;
assume A4:
A is
mono
;
F is one-to-one
assume
not
F is
one-to-one
;
contradiction
then consider x1,
x2 being
object such that A5:
x1 in dom F
and A6:
x2 in dom F
and A7:
F . x1 = F . x2
and A8:
x1 <> x2
by FUNCT_1:def 4;
set C =
o1 --> x2;
set B =
o1 --> x1;
A9:
dom (o1 --> x2) = o1
by FUNCOP_1:13;
A10:
rng (o1 --> x2) c= o1
then A11:
dom (F * (o1 --> x2)) = o1
by A3, A9, RELAT_1:27;
o1 --> x2 in Funcs (
o1,
o1)
by A9, A10, FUNCT_2:def 2;
then reconsider C1 =
o1 --> x2 as
Morphism of
o1,
o1 by ALTCAT_1:def 14;
set o9 = the
Element of
o1;
A12:
<^o1,o1^> <> {}
by ALTCAT_1:19;
(o1 --> x1) . the
Element of
o1 = x1
by A3, A5, FUNCOP_1:7;
then A13:
(o1 --> x1) . the
Element of
o1 <> (o1 --> x2) . the
Element of
o1
by A3, A5, A8, FUNCOP_1:7;
A14:
dom (o1 --> x1) = o1
by FUNCOP_1:13;
A15:
rng (o1 --> x1) c= o1
then
o1 --> x1 in Funcs (
o1,
o1)
by A14, FUNCT_2:def 2;
then reconsider B1 =
o1 --> x1 as
Morphism of
o1,
o1 by ALTCAT_1:def 14;
A16:
dom (F * (o1 --> x1)) = o1
by A3, A14, A15, RELAT_1:27;
then
F * (o1 --> x1) = F * (o1 --> x2)
by A16, A11, FUNCT_1:2;
then A * B1 =
F * (o1 --> x2)
by A1, A2, A12, ALTCAT_1:16
.=
A * C1
by A1, A2, A12, ALTCAT_1:16
;
hence
contradiction
by A4, A12, A13;
verum
end; thus
(
F is
one-to-one implies
A is
mono )
verumproof
assume A18:
F is
one-to-one
;
A is mono
let o be
Object of
(EnsCat X);
ALTCAT_3:def 7 ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A19:
<^o,o1^> <> {}
;
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
then A20:
<^o,o2^> <> {}
by A1, ALTCAT_1:def 2;
let B,
C be
Morphism of
o,
o1;
( A * B = A * C implies B = C )
A21:
<^o,o1^> = Funcs (
o,
o1)
by ALTCAT_1:def 14;
then consider B1 being
Function such that A22:
B1 = B
and A23:
dom B1 = o
and A24:
rng B1 c= o1
by A19, FUNCT_2:def 2;
consider C1 being
Function such that A25:
C1 = C
and A26:
dom C1 = o
and A27:
rng C1 c= o1
by A19, A21, FUNCT_2:def 2;
assume
A * B = A * C
;
B = C
then A28:
F * B1 =
A * C
by A1, A2, A19, A22, A20, ALTCAT_1:16
.=
F * C1
by A1, A2, A19, A25, A20, ALTCAT_1:16
;
now for z being object st z in o holds
B1 . z = C1 . zlet z be
object ;
( z in o implies B1 . z = C1 . z )assume A29:
z in o
;
B1 . z = C1 . zthen
F . (B1 . z) = (F * B1) . z
by A23, FUNCT_1:13;
then A30:
F . (B1 . z) = F . (C1 . z)
by A26, A28, A29, FUNCT_1:13;
(
B1 . z in rng B1 &
C1 . z in rng C1 )
by A23, A26, A29, FUNCT_1:def 3;
hence
B1 . z = C1 . z
by A3, A18, A24, A27, A30, FUNCT_1:def 4;
verum end;
hence
B = C
by A22, A23, A25, A26, FUNCT_1:2;
verum
end; end; suppose A31:
o2 = {}
;
( A is mono iff F is one-to-one )then
F = {}
;
hence
(
A is
mono implies
F is
one-to-one )
;
( F is one-to-one implies A is mono )thus
(
F is
one-to-one implies
A is
mono )
verumproof
set x = the
Element of
Funcs (
o1,
o2);
assume
F is
one-to-one
;
A is mono
let o be
Object of
(EnsCat X);
ALTCAT_3:def 7 ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A32:
<^o,o1^> <> {}
;
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
<^o1,o2^> = Funcs (
o1,
o2)
by ALTCAT_1:def 14;
then consider f being
Function such that
f = the
Element of
Funcs (
o1,
o2)
and A33:
dom f = o1
and A34:
rng f c= o2
by A1, FUNCT_2:def 2;
let B,
C be
Morphism of
o,
o1;
( A * B = A * C implies B = C )
A35:
<^o,o1^> = Funcs (
o,
o1)
by ALTCAT_1:def 14;
then consider B1 being
Function such that A36:
B1 = B
and A37:
dom B1 = o
and A38:
rng B1 c= o1
by A32, FUNCT_2:def 2;
rng f = {}
by A31, A34, XBOOLE_1:3;
then
dom f = {}
by RELAT_1:42;
then A39:
rng B1 = {}
by A38, A33, XBOOLE_1:3;
then A40:
dom B1 = {}
by RELAT_1:42;
assume
A * B = A * C
;
B = C
consider C1 being
Function such that A41:
C1 = C
and A42:
dom C1 = o
and
rng C1 c= o1
by A32, A35, FUNCT_2:def 2;
B1 =
{}
by A39, RELAT_1:41
.=
C1
by A37, A42, A40, RELAT_1:41
;
hence
B = C
by A36, A41;
verum
end; end;