let V be non empty set ; for W being non empty Subset of V holds Ens W is Subcategory of Ens V
let W be non empty Subset of V; Ens W is Subcategory of Ens V
A1:
for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a,
b be
Object of
(Ens W);
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)let a9,
b9 be
Object of
(Ens V);
( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A2:
(
a = a9 &
b = b9 )
;
Hom (a,b) = Hom (a9,b9)
(
Hom (
a,
b)
= Maps (
(@ a),
(@ b)) &
Hom (
a9,
b9)
= Maps (
(@ a9),
(@ b9)) )
by Th26;
hence
Hom (
a,
b)
= Hom (
a9,
b9)
by A2, Lm5;
verum
end;
set w = the Comp of (Ens W);
set v = the Comp of (Ens V);
thus
the carrier of (Ens W) c= the carrier of (Ens V)
; CAT_2:def 4 ( ( for b1, b2 being Element of the carrier of (Ens W)
for b3, b4 being Element of the carrier of (Ens V) holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (Ens W) c= the Comp of (Ens V) & ( for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus
for a, b being Object of (Ens W)
for a9, b9 being Object of (Ens V) st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
by A1; ( the Comp of (Ens W) c= the Comp of (Ens V) & ( for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 ) ) )
now ( dom the Comp of (Ens W) c= dom the Comp of (Ens V) & ( for x being object st x in dom the Comp of (Ens W) holds
the Comp of (Ens W) . x = the Comp of (Ens V) . x ) )A3:
dom the
Comp of
(Ens W) c= [:(Maps W),(Maps W):]
by RELAT_1:def 18;
thus A4:
dom the
Comp of
(Ens W) c= dom the
Comp of
(Ens V)
for x being object st x in dom the Comp of (Ens W) holds
the Comp of (Ens W) . x = the Comp of (Ens V) . xproof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in dom the Comp of (Ens W) or [x,y] in dom the Comp of (Ens V) )
assume A5:
[x,y] in dom the
Comp of
(Ens W)
;
[x,y] in dom the Comp of (Ens V)
then consider m2,
m1 being
Element of
Maps W such that A6:
[x,y] = [m2,m1]
by A3, DOMAIN_1:1;
reconsider m19 =
m1,
m29 =
m2 as
Element of
Maps V by Th7, TARSKI:def 3;
A7:
(
dom m29 = dom m2 &
cod m19 = cod m1 )
;
dom m2 = cod m1
by A5, A6, Def11;
hence
[x,y] in dom the
Comp of
(Ens V)
by A6, A7, Def11;
verum
end; let x be
object ;
( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )assume A8:
x in dom the
Comp of
(Ens W)
;
the Comp of (Ens W) . x = the Comp of (Ens V) . xthen consider m2,
m1 being
Element of
Maps W such that A9:
x = [m2,m1]
by A3, DOMAIN_1:1;
reconsider m19 =
m1,
m29 =
m2 as
Element of
Maps V by Th7, TARSKI:def 3;
A10:
dom m29 = cod m19
by A4, A8, A9, Def11;
A11:
dom m2 = cod m1
by A8, A9, Def11;
then A12:
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]
by Def6;
(
dom m1 = dom m19 &
cod m2 = cod m29 )
;
then
m29 * m19 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]
by A10, Def6;
hence the
Comp of
(Ens W) . x =
m29 * m19
by A9, A11, A12, Def11
.=
the
Comp of
(Ens V) . x
by A9, A10, Def11
;
verum end;
hence
the Comp of (Ens W) c= the Comp of (Ens V)
by GRFUNC_1:2; for b1 being Element of the carrier of (Ens W)
for b2 being Element of the carrier of (Ens V) holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of (Ens W); for b1 being Element of the carrier of (Ens V) holds
( not a = b1 or id a = id b1 )
let a9 be Object of (Ens V); ( not a = a9 or id a = id a9 )
A13:
id$ (@ a) = [[(@ a),(@ a)],(id (@ a))]
;
assume
a = a9
; id a = id a9
hence id a =
id$ (@ a9)
by A13, Th28
.=
id a9
by Th28
;
verum