let V be non empty set ; for W being non empty Subset of V holds Ens W is_full_subcategory_of Ens V
let W be non empty Subset of V; Ens W is_full_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 Th27;
hence
Hom (
a,
b)
= Hom (
a9,
b9)
by A2, Lm5;
verum
end;
thus
Ens W is Subcategory of Ens V
CAT_2:def 6 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) = Hom (b3,b4) )proof
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 A3:
dom the
Comp of
(Ens W) c= [:(Maps W),(Maps W):]
by RELAT_1:def 18;
A4:
Maps W c= Maps V
by Th7;
thus A5:
dom the
Comp of
(Ens W) c= dom the
Comp of
(Ens V)
for x being set 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
set ;
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 A6:
[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 A7:
[x,y] = [m2,m1]
by A3, DOMAIN_1:9;
reconsider m19 =
m1,
m29 =
m2 as
Element of
Maps V by A4, TARSKI:def 3;
A8:
(
dom m29 = dom m2 &
cod m19 = cod m1 )
;
dom m2 = cod m1
by A6, A7, Def12;
hence
[x,y] in dom the
Comp of
(Ens V)
by A7, A8, Def12;
verum
end; let x be
set ;
( x in dom the Comp of (Ens W) implies the Comp of (Ens W) . x = the Comp of (Ens V) . x )assume A9:
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 A10:
x = [m2,m1]
by A3, DOMAIN_1:9;
reconsider m19 =
m1,
m29 =
m2 as
Element of
Maps V by A4, TARSKI:def 3;
A11:
dom m29 = cod m19
by A5, A9, A10, Def12;
A12:
dom m2 = cod m1
by A9, A10, Def12;
then A13:
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]
by Def7;
(
dom m1 = dom m19 &
cod m2 = cod m29 )
;
then
m29 * m19 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))]
by A11, Def7;
hence the
Comp of
(Ens W) . x =
m29 * m19
by A10, A12, A13, Def12
.=
the
Comp of
(Ens V) . x
by A10, A11, Def12
;
verum end;
hence
the
Comp of
(Ens W) c= the
Comp of
(Ens V)
by GRFUNC_1:8;
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 )
A14:
id$ (@ a) = [[(@ a),(@ a)],(id (@ a))]
;
assume
a = a9
;
id a = id a9
hence id a =
id$ (@ a9)
by A14, Def13
.=
id a9
by Def13
;
verum
end;
thus
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) = Hom (b3,b4) )
by A1; verum