defpred S1[ set , set ] means ex f being Covariant bifunction of the carrier of A,the carrier of B ex m being MSUnTrans of f,the Arrows of A,the Arrows of B st
( $1 = [f,m] & $2 = FunctorStr(# f,m #) & $2 is covariant Functor of A,B );
A1:
for x, y, z being set st S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
set ;
:: thesis: ( S1[x,y] & S1[x,z] implies y = z )
given f being
Covariant bifunction of the
carrier of
A,the
carrier of
B,
m being
MSUnTrans of
f,the
Arrows of
A,the
Arrows of
B such that A2:
(
x = [f,m] &
y = FunctorStr(#
f,
m #) &
y is
covariant Functor of
A,
B )
;
:: thesis: ( not S1[x,z] or y = z )
given f1 being
Covariant bifunction of the
carrier of
A,the
carrier of
B,
m1 being
MSUnTrans of
f1,the
Arrows of
A,the
Arrows of
B such that A3:
(
x = [f1,m1] &
z = FunctorStr(#
f1,
m1 #) &
z is
covariant Functor of
A,
B )
;
:: thesis: y = z
(
f = f1 &
m = m1 )
by A2, A3, ZFMISC_1:33;
hence
y = z
by A2, A3;
:: thesis: verum
end;
set A' = Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:];
set sAA = { (the Arrows of B * f) where f is Element of Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:] : verum } ;
consider f being Element of Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:];
the Arrows of B * f in { (the Arrows of B * f) where f is Element of Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:] : verum }
;
then reconsider sAA = { (the Arrows of B * f) where f is Element of Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:] : verum } as non empty set ;
defpred S2[ set , set ] means ex AA being ManySortedSet of [:the carrier of A,the carrier of A:] st
( $1 = AA & $2 = Funcs the Arrows of A,AA );
A4:
for x, y, z being set st S2[x,y] & S2[x,z] holds
y = z
;
consider XX being set such that
A5:
for x being set holds
( x in XX iff ex y being set st
( y in sAA & S2[y,x] ) )
from TARSKI:sch 1(A4);
consider X being set such that
A6:
for x being set holds
( x in X iff ex y being set st
( y in [:(Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:]),(union XX):] & S1[y,x] ) )
from TARSKI:sch 1(A1);
take
X
; :: thesis: for x being set holds
( x in X iff x is strict covariant Functor of A,B )
let x be set ; :: thesis: ( x in X iff x is strict covariant Functor of A,B )
thus
( x in X implies x is strict covariant Functor of A,B )
:: thesis: ( x is strict covariant Functor of A,B implies x in X )proof
assume
x in X
;
:: thesis: x is strict covariant Functor of A,B
then
ex
y being
set st
(
y in [:(Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:]),(union XX):] & ex
f being
Covariant bifunction of the
carrier of
A,the
carrier of
B ex
m being
MSUnTrans of
f,the
Arrows of
A,the
Arrows of
B st
(
y = [f,m] &
x = FunctorStr(#
f,
m #) &
x is
covariant Functor of
A,
B ) )
by A6;
hence
x is
strict covariant Functor of
A,
B
;
:: thesis: verum
end;
assume
x is strict covariant Functor of A,B
; :: thesis: x in X
then reconsider F = x as strict covariant Functor of A,B ;
reconsider f = the ObjectMap of F as Covariant bifunction of the carrier of A,the carrier of B by FUNCTOR0:def 13;
A7:
for o1, o2 being object of A st the Arrows of A . o1,o2 <> {} holds
the Arrows of B . (f . o1,o2) <> {}
A9:
for o1, o2 being object of A st the Arrows of A . o1,o2 <> {} holds
the Arrows of B . [(F . o1),(F . o2)] <> {}
reconsider m = the MorphMap of F as MSUnTrans of f,the Arrows of A,the Arrows of B ;
reconsider y = [f,m] as set ;
y in [:(Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:]),(union XX):]
proof
A11:
f in Funcs [:the carrier of A,the carrier of A:],
[:the carrier of B,the carrier of B:]
by FUNCT_2:11;
then A12:
the
Arrows of
B * f in sAA
;
reconsider AA = the
Arrows of
B * f as
ManySortedSet of
[:the carrier of A,the carrier of A:] ;
set I =
[:the carrier of A,the carrier of A:];
A13:
m is
ManySortedFunction of the
Arrows of
A,
AA
by FUNCTOR0:def 5;
A14:
for
i being
set st
i in [:the carrier of A,the carrier of A:] & the
Arrows of
A . i <> {} holds
the
Arrows of
B . (f . i) <> {}
proof
let i be
set ;
:: thesis: ( i in [:the carrier of A,the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (f . i) <> {} )
assume that A15:
i in [:the carrier of A,the carrier of A:]
and A16:
the
Arrows of
A . i <> {}
;
:: thesis: the Arrows of B . (f . i) <> {}
consider o1,
o2 being
set such that A17:
o1 in the
carrier of
A
and A18:
o2 in the
carrier of
A
and A19:
i = [o1,o2]
by A15, ZFMISC_1:def 2;
reconsider a1 =
o1,
a2 =
o2 as
object of
A by A17, A18;
A20: the
Arrows of
B . (f . i) =
the
Arrows of
B . (f . o1,o2)
by A19
.=
the
Arrows of
B . [(F . a1),(F . a2)]
by FUNCTOR0:23
;
the
Arrows of
A . o1,
o2 <> {}
by A16, A19;
hence
the
Arrows of
B . (f . i) <> {}
by A9, A20;
:: thesis: verum
end;
for
i being
set st
i in [:the carrier of A,the carrier of A:] & the
Arrows of
A . i <> {} holds
AA . i <> {}
then
for
i being
set st
i in [:the carrier of A,the carrier of A:] &
AA . i = {} holds
the
Arrows of
A . i = {}
;
then A23:
m in Funcs the
Arrows of
A,
AA
by A13, Def9;
Funcs the
Arrows of
A,
AA in XX
by A5, A12;
then
m in union XX
by A23, TARSKI:def 4;
hence
y in [:(Funcs [:the carrier of A,the carrier of A:],[:the carrier of B,the carrier of B:]),(union XX):]
by A11, ZFMISC_1:def 2;
:: thesis: verum
end;
hence
x in X
by A6; :: thesis: verum