let C be Category; :: thesis: for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let M be non empty set ; :: thesis: for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let d, c be Function of M,O; :: thesis: for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is full Subcategory of C
let i be Function of O,M; :: thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is full Subcategory of C )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
assume that
A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; :: thesis: CatStr(# O,M,d,c,p #) is full Subcategory of C
set B = CatStr(# O,M,d,c,p #);
A5: now :: thesis: for f being Morphism of CatStr(# O,M,d,c,p #) holds f is Morphism of C
let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: f is Morphism of C
consider X being set such that
A6: f in X and
A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;
ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence f is Morphism of C by A6; :: thesis: verum
end;
A8: for a, b being Object of CatStr(# O,M,d,c,p #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a, b be Object of CatStr(# O,M,d,c,p #); :: thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A9: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)
now :: thesis: for x being object holds
( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )
let x be object ; :: thesis: ( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )
thus ( x in Hom (a,b) implies x in Hom (a9,b9) ) :: thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )
proof
assume A10: x in Hom (a,b) ; :: thesis: x in Hom (a9,b9)
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;
reconsider f9 = f as Morphism of C by A5;
cod f = cod f9 by A3, FUNCT_1:49;
then A11: b = cod f9 by A10, CAT_1:1;
dom f = dom f9 by A2, FUNCT_1:49;
then a = dom f9 by A10, CAT_1:1;
hence x in Hom (a9,b9) by A9, A11; :: thesis: verum
end;
assume A12: x in Hom (a9,b9) ; :: thesis: x in Hom (a,b)
then reconsider f9 = x as Morphism of C ;
Hom (a9,b9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A9;
then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def 4;
cod f = cod f9 by A3, FUNCT_1:49;
then A13: cod f = b9 by A12, CAT_1:1;
dom f = dom f9 by A2, FUNCT_1:49;
then dom f = a9 by A12, CAT_1:1;
hence x in Hom (a,b) by A9, A13; :: thesis: verum
end;
hence Hom (a,b) = Hom (a9,b9) by TARSKI:2; :: thesis: verum
end;
reconsider B = CatStr(# O,M,d,c,p #) as Subcategory of C by Lm2, A1, A2, A3, A4;
B is full by A8;
hence CatStr(# O,M,d,c,p #) is full Subcategory of C ; :: thesis: verum