set F = F3();
thus
the ObjectMap of F3() is one-to-one
FUNCTOR0:def 6,FUNCTOR0:def 33,FUNCTOR0:def 35 ( F3() is faithful & F3() is surjective,F2()) )proof
let x1,
x2,
y1,
y2 be
Element of
F1();
YELLOW18:def 1 ( the ObjectMap of F3() . (x1,y1) = the ObjectMap of F3() . (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
reconsider a1 =
x1,
a2 =
x2,
b1 =
y1,
b2 =
y2 as
Object of
F1() ;
assume
the
ObjectMap of
F3()
. (
x1,
y1)
= the
ObjectMap of
F3()
. (
x2,
y2)
;
( x1 = x2 & y1 = y2 )
then A6:
[(F3() . a1),(F3() . b1)] =
the
ObjectMap of
F3()
. (
x2,
y2)
by FUNCTOR0:22
.=
[(F3() . a2),(F3() . b2)]
by FUNCTOR0:22
;
then A7:
F3()
. a1 = F3()
. a2
by XTUPLE_0:1;
A8:
F3()
. b1 = F3()
. b2
by A6, XTUPLE_0:1;
A9:
F4(
a1)
= F3()
. a2
by A1, A7;
A10:
F4(
b1)
= F3()
. b2
by A1, A8;
A11:
F4(
a1)
= F4(
a2)
by A1, A9;
F4(
b1)
= F4(
b2)
by A1, A10;
hence
(
x1 = x2 &
y1 = y2 )
by A3, A11;
verum
end;
now for i being set st i in [: the carrier of F1(), the carrier of F1():] holds
the MorphMap of F3() . i is one-to-one let i be
set ;
( i in [: the carrier of F1(), the carrier of F1():] implies the MorphMap of F3() . i is one-to-one )assume
i in [: the carrier of F1(), the carrier of F1():]
;
the MorphMap of F3() . i is one-to-one then consider a,
b being
object such that A12:
a in the
carrier of
F1()
and A13:
b in the
carrier of
F1()
and A14:
i = [a,b]
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Object of
F1()
by A12, A13;
A15:
(
<^a,b^> <> {} implies
<^(F3() . a),(F3() . b)^> <> {} )
by FUNCTOR0:def 18;
Morph-Map (
F3(),
a,
b) is
one-to-one
proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in proj1 (Morph-Map (F3(),a,b)) or not y in proj1 (Morph-Map (F3(),a,b)) or not (Morph-Map (F3(),a,b)) . x = (Morph-Map (F3(),a,b)) . y or x = y )
assume that A16:
x in dom (Morph-Map (F3(),a,b))
and A17:
y in dom (Morph-Map (F3(),a,b))
;
( not (Morph-Map (F3(),a,b)) . x = (Morph-Map (F3(),a,b)) . y or x = y )
reconsider f =
x,
g =
y as
Morphism of
a,
b by A16, A17;
A18:
F3()
. f = (Morph-Map (F3(),a,b)) . x
by A15, A16, FUNCTOR0:def 15;
A19:
F3()
. g = (Morph-Map (F3(),a,b)) . y
by A15, A16, FUNCTOR0:def 15;
A20:
F5(
a,
b,
f)
= (Morph-Map (F3(),a,b)) . x
by A2, A16, A18;
F5(
a,
b,
g)
= (Morph-Map (F3(),a,b)) . y
by A2, A16, A19;
hence
( not
(Morph-Map (F3(),a,b)) . x = (Morph-Map (F3(),a,b)) . y or
x = y )
by A4, A16, A20;
verum
end; hence
the
MorphMap of
F3()
. i is
one-to-one
by A14;
verum end;
hence
the MorphMap of F3() is "1-1"
by MSUALG_3:1; FUNCTOR0:def 30 F3() is surjective,F2())
reconsider G = the MorphMap of F3() as ManySortedFunction of the Arrows of F1(), the Arrows of F2() * the ObjectMap of F3() by FUNCTOR0:def 4;
thus
F3() is full
FUNCTOR0:def 34 F3() is onto proof
take
G
;
FUNCTOR0:def 32 ( G = the MorphMap of F3() & G is "onto" )
thus
G = the
MorphMap of
F3()
;
G is "onto"
let i be
set ;
MSUALG_3:def 3 ( not i in [: the carrier of F1(), the carrier of F1():] or proj2 (G . i) = ( the ObjectMap of F3() (#) the Arrows of F2()) . i )
assume
i in [: the carrier of F1(), the carrier of F1():]
;
proj2 (G . i) = ( the ObjectMap of F3() (#) the Arrows of F2()) . i
then reconsider ab =
i as
Element of
[: the carrier of F1(), the carrier of F1():] ;
G . ab is
Function of
( the Arrows of F1() . ab),
(( the Arrows of F2() * the ObjectMap of F3()) . ab)
;
hence
rng (G . i) c= ( the Arrows of F2() * the ObjectMap of F3()) . i
by RELAT_1:def 19;
XBOOLE_0:def 10 ( the ObjectMap of F3() (#) the Arrows of F2()) . i c= proj2 (G . i)
consider a,
b being
object such that A21:
a in the
carrier of
F1()
and A22:
b in the
carrier of
F1()
and A23:
ab = [a,b]
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
Object of
F1()
by A21, A22;
A24: the
ObjectMap of
F3()
. ab =
the
ObjectMap of
F3()
. (
a,
b)
by A23
.=
[(F3() . a),(F3() . b)]
by FUNCTOR0:22
;
then A25:
( the Arrows of F2() * the ObjectMap of F3()) . ab = <^(F3() . a),(F3() . b)^>
by FUNCT_2:15;
let x be
object ;
TARSKI:def 3 ( not x in ( the ObjectMap of F3() (#) the Arrows of F2()) . i or x in proj2 (G . i) )
assume A26:
x in ( the Arrows of F2() * the ObjectMap of F3()) . i
;
x in proj2 (G . i)
then reconsider f =
x as
Morphism of
(F3() . a),
(F3() . b) by A24, FUNCT_2:15;
consider c,
d being
Object of
F1(),
g being
Morphism of
c,
d such that A27:
F3()
. a = F4(
c)
and A28:
F3()
. b = F4(
d)
and A29:
<^c,d^> <> {}
and A30:
f = F5(
c,
d,
g)
by A5, A25, A26;
A31:
F4(
a)
= F4(
c)
by A1, A27;
A32:
F4(
b)
= F4(
d)
by A1, A28;
A33:
a = c
by A3, A31;
A34:
b = d
by A3, A32;
A35:
f =
F3()
. g
by A2, A29, A30
.=
(Morph-Map (F3(),c,d)) . g
by A25, A26, A29, A33, A34, FUNCTOR0:def 15
;
dom (Morph-Map (F3(),a,b)) = <^a,b^>
by A25, A26, FUNCT_2:def 1;
hence
x in proj2 (G . i)
by A23, A29, A33, A34, A35, FUNCT_1:def 3;
verum
end;
thus
rng the ObjectMap of F3() c= [: the carrier of F2(), the carrier of F2():]
; FUNCTOR0:def 7,FUNCT_2:def 3,XBOOLE_0:def 10 [: the carrier of F2(), the carrier of F2():] c= rng the ObjectMap of F3()
let x be object ; TARSKI:def 3 ( not x in [: the carrier of F2(), the carrier of F2():] or x in rng the ObjectMap of F3() )
assume
x in [: the carrier of F2(), the carrier of F2():]
; x in rng the ObjectMap of F3()
then consider a, b being object such that
A36:
a in the carrier of F2()
and
A37:
b in the carrier of F2()
and
A38:
x = [a,b]
by ZFMISC_1:def 2;
reconsider a = a, b = b as Object of F2() by A36, A37;
consider c, c9 being Object of F1(), g being Morphism of c,c9 such that
A39:
a = F4(c)
and
a = F4(c9)
and
<^c,c9^> <> {}
and
idm a = F5(c,c9,g)
by A5;
consider d, d9 being Object of F1(), h being Morphism of d,d9 such that
A40:
b = F4(d)
and
b = F4(d9)
and
<^d,d9^> <> {}
and
idm b = F5(d,d9,h)
by A5;
[c,d] in [: the carrier of F1(), the carrier of F1():]
by ZFMISC_1:def 2;
then A41:
[c,d] in dom the ObjectMap of F3()
by FUNCT_2:def 1;
the ObjectMap of F3() . [c,d] =
the ObjectMap of F3() . (c,d)
.=
[(F3() . c),(F3() . d)]
by FUNCTOR0:22
.=
[a,(F3() . d)]
by A1, A39
.=
x
by A1, A38, A40
;
hence
x in rng the ObjectMap of F3()
by A41, FUNCT_1:def 3; verum