let C, D be Categorial Category; ( the carrier' of C c= the carrier' of D implies C is Subcategory of D )
assume A1:
the carrier' of C c= the carrier' of D
; C is Subcategory of D
thus
the carrier of C c= the carrier of D
CAT_2:def 4 ( ( for b1, b2 being Element of the carrier of C
for b3, b4 being Element of the carrier of D holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 ) ) )
hereby ( the Comp of C c= the Comp of D & ( for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 ) ) )
let a,
b be
Object of
C;
for a9, b9 being Object of D st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)let a9,
b9 be
Object of
D;
( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )assume that A3:
a = a9
and A4:
b = b9
;
Hom (a,b) c= Hom (a9,b9)thus
Hom (
a,
b)
c= Hom (
a9,
b9)
verumproof
let x be
object ;
TARSKI:def 3 ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume
x in Hom (
a,
b)
;
x in Hom (a9,b9)
then consider f being
Morphism of
C such that A5:
x = f
and A6:
dom f = a
and A7:
cod f = b
;
reconsider A =
a,
B =
b as
Category by Th12;
A8:
ex
F being
Functor of
A,
B st
f = [[A,B],F]
by A6, A7, Def6;
reconsider f =
f as
Morphism of
D by A1;
A9:
dom f = f `11
by Th13;
A10:
cod f = f `12
by Th13;
A11:
f `11 = A
by A8, MCART_1:85;
f `12 = B
by A8, MCART_1:85;
hence
x in Hom (
a9,
b9)
by A3, A4, A5, A9, A10, A11;
verum
end;
end;
A12:
dom the Comp of C c= dom the Comp of D
proof
let x be
object ;
TARSKI:def 3 ( not x in dom the Comp of C or x in dom the Comp of D )
assume A13:
x in dom the
Comp of
C
;
x in dom the Comp of D
then reconsider g =
x `1 ,
f =
x `2 as
Morphism of
C by MCART_1:10;
reconsider g9 =
g,
f9 =
f as
Morphism of
D by A1;
A14:
x = [g,f]
by A13, MCART_1:21;
then A15:
dom g = cod f
by A13, CAT_1:15;
A16:
dom g = g `11
by Th13;
A17:
dom g9 = g `11
by Th13;
A18:
cod f = f `12
by Th13;
cod f9 = f `12
by Th13;
hence
x in dom the
Comp of
D
by A14, A15, A16, A17, A18, CAT_1:15;
verum
end;
now for x being object st x in dom the Comp of C holds
the Comp of C . x = the Comp of D . xlet x be
object ;
( x in dom the Comp of C implies the Comp of C . x = the Comp of D . x )assume A19:
x in dom the
Comp of
C
;
the Comp of C . x = the Comp of D . xthen reconsider g =
x `1 ,
f =
x `2 as
Morphism of
C by MCART_1:10;
reconsider g9 =
g,
f9 =
f as
Morphism of
D by A1;
A20:
x = [g,f]
by A19, MCART_1:21;
A21:
dom g = g `11
by Th13;
cod g = g `12
by Th13;
then consider G being
Functor of
g `11 ,
g `12 such that A22:
g = [[(g `11),(g `12)],G]
by A21, Def6;
A23:
dom f = f `11
by Th13;
cod f = dom g
by A19, A20, CAT_1:15;
then consider F being
Functor of
f `11 ,
g `11 such that A24:
f = [[(f `11),(g `11)],F]
by A21, A23, Def6;
thus the
Comp of
C . x =
the
Comp of
C . (
g,
f)
by A19, MCART_1:21
.=
g (*) f
by A19, A20, CAT_1:def 1
.=
[[(f `11),(g `12)],(G * F)]
by A22, A24, Def6
.=
g9 (*) f9
by A22, A24, Def6
.=
the
Comp of
D . (
g,
f)
by A12, A19, A20, CAT_1:def 1
.=
the
Comp of
D . x
by A19, MCART_1:21
;
verum end;
hence
the Comp of C c= the Comp of D
by A12, GRFUNC_1:2; for b1 being Element of the carrier of C
for b2 being Element of the carrier of D holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of C; for b1 being Element of the carrier of D holds
( not a = b1 or id a = id b1 )
let a9 be Object of D; ( not a = a9 or id a = id a9 )
assume A25:
a = a9
; id a = id a9
reconsider A = a as Category by Th12;
thus id a =
[[A,A],(id A)]
by Def6
.=
id a9
by A25, Def6
; verum