set F = F3();
thus
the ObjectMap of F3() is one-to-one
:: according to FUNCTOR0:def 7,FUNCTOR0:def 34,FUNCTOR0:def 36 :: thesis: ( F3() is faithful & F3() is V184(F1(),F2()) )proof
let x1,
x2,
y1,
y2 be
Element of
F1();
:: according to YELLOW18:def 1 :: thesis: ( 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
;
:: thesis: ( x1 = x2 & y1 = y2 )
then [(F3() . a1),(F3() . b1)] =
the
ObjectMap of
F3()
. x2,
y2
by FUNCTOR0:23
.=
[(F3() . a2),(F3() . b2)]
by FUNCTOR0:23
;
then
(
F3()
. a1 = F3()
. a2 &
F3()
. b1 = F3()
. b2 )
by ZFMISC_1:33;
then
(
F4(
a1)
= F3()
. a2 &
F4(
b1)
= F3()
. b2 )
by A1;
then
(
F4(
a1)
= F4(
a2) &
F4(
b1)
= F4(
b2) )
by A1;
hence
(
x1 = x2 &
y1 = y2 )
by A3;
:: thesis: verum
end;
now let i be
set ;
:: thesis: ( 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():]
;
:: thesis: the MorphMap of F3() . i is one-to-one then consider a,
b being
set such that A6:
(
a in the
carrier of
F1() &
b in the
carrier of
F1() &
i = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
object of
F1()
by A6;
A7:
(
<^a,b^> <> {} implies
<^(F3() . a),(F3() . b)^> <> {} )
by FUNCTOR0:def 19;
Morph-Map F3(),
a,
b is
one-to-one
proof
let x,
y be
set ;
:: according to FUNCT_1:def 8 :: thesis: ( 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 A8:
(
x in dom (Morph-Map F3(),a,b) &
y in dom (Morph-Map F3(),a,b) )
;
:: thesis: ( not (Morph-Map F3(),a,b) . x = (Morph-Map F3(),a,b) . y or x = y )
then reconsider f =
x,
g =
y as
Morphism of
a,
b ;
(
F3()
. f = (Morph-Map F3(),a,b) . x &
F3()
. g = (Morph-Map F3(),a,b) . y )
by A7, A8, FUNCTOR0:def 16;
then
(
F5(
a,
b,
f)
= (Morph-Map F3(),a,b) . x &
F5(
a,
b,
g)
= (Morph-Map F3(),a,b) . y )
by A2, A8;
hence
( not
(Morph-Map F3(),a,b) . x = (Morph-Map F3(),a,b) . y or
x = y )
by A4, A8;
:: thesis: verum
end; hence
the
MorphMap of
F3()
. i is
one-to-one
by A6;
:: thesis: verum end;
hence
the MorphMap of F3() is "1-1"
by MSUALG_3:1; :: according to FUNCTOR0:def 31 :: thesis: F3() is V184(F1(),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 5;
thus
F3() is full
:: according to FUNCTOR0:def 35 :: thesis: F3() is onto proof
take
G
;
:: according to FUNCTOR0:def 33 :: thesis: ( G = the MorphMap of F3() & G is "onto" )
thus
G = the
MorphMap of
F3()
;
:: thesis: G is "onto"
let i be
set ;
:: according to MSUALG_3:def 3 :: thesis: ( 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():]
;
:: thesis: 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;
:: according to XBOOLE_0:def 10 :: thesis: (the ObjectMap of F3() * the Arrows of F2()) . i c= proj2 (G . i)
consider a,
b being
set such that A9:
(
a in the
carrier of
F1() &
b in the
carrier of
F1() &
ab = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a,
b =
b as
object of
F1()
by A9;
A10: the
ObjectMap of
F3()
. ab =
the
ObjectMap of
F3()
. a,
b
by A9
.=
[(F3() . a),(F3() . b)]
by FUNCTOR0:23
;
then A11:
(the Arrows of F2() * the ObjectMap of F3()) . ab = <^(F3() . a),(F3() . b)^>
by FUNCT_2:21;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (the ObjectMap of F3() * the Arrows of F2()) . i or x in proj2 (G . i) )
assume A12:
x in (the Arrows of F2() * the ObjectMap of F3()) . i
;
:: thesis: x in proj2 (G . i)
then reconsider f =
x as
Morphism of
(F3() . a),
(F3() . b) by A10, FUNCT_2:21;
consider c,
d being
object of
F1(),
g being
Morphism of
c,
d such that A13:
(
F3()
. a = F4(
c) &
F3()
. b = F4(
d) &
<^c,d^> <> {} &
f = F5(
c,
d,
g) )
by A5, A11, A12;
(
F4(
a)
= F4(
c) &
F4(
b)
= F4(
d) )
by A1, A13;
then A14:
(
a = c &
b = d )
by A3;
A15:
f =
F3()
. g
by A2, A13
.=
(Morph-Map F3(),c,d) . g
by A11, A12, A13, A14, FUNCTOR0:def 16
;
(
dom (Morph-Map F3(),a,b) = <^a,b^> &
G . ab = Morph-Map F3(),
a,
b )
by A9, A11, A12, FUNCT_2:def 1;
hence
x in proj2 (G . i)
by A13, A14, A15, FUNCT_1:def 5;
:: thesis: verum
end;
thus
rng the ObjectMap of F3() c= [:the carrier of F2(),the carrier of F2():]
; :: according to FUNCTOR0:def 8,FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: [:the carrier of F2(),the carrier of F2():] c= proj2 the ObjectMap of F3()
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:the carrier of F2(),the carrier of F2():] or x in proj2 the ObjectMap of F3() )
assume
x in [:the carrier of F2(),the carrier of F2():]
; :: thesis: x in proj2 the ObjectMap of F3()
then consider a, b being set such that
A16:
( a in the carrier of F2() & b in the carrier of F2() & x = [a,b] )
by ZFMISC_1:def 2;
reconsider a = a, b = b as object of F2() by A16;
consider c, c' being object of F1(), g being Morphism of c,c' such that
A17:
( a = F4(c) & a = F4(c') & <^c,c'^> <> {} & idm a = F5(c,c',g) )
by A5;
consider d, d' being object of F1(), h being Morphism of d,d' such that
A18:
( b = F4(d) & b = F4(d') & <^d,d'^> <> {} & idm b = F5(d,d',h) )
by A5;
[c,d] in [:the carrier of F1(),the carrier of F1():]
by ZFMISC_1:def 2;
then A19:
[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:23
.=
[a,(F3() . d)]
by A1, A17
.=
x
by A1, A16, A18
;
hence
x in proj2 the ObjectMap of F3()
by A19, FUNCT_1:def 5; :: thesis: verum