set a = the Object of C;
A1: dom (Obj F) = the carrier of C by FUNCT_2:def 1;
then (Obj F) . the Object of C in rng (Obj F) by FUNCT_1:def 3;
then reconsider O = rng (Obj F) as non empty set ;
reconsider O = O as non empty Subset of the carrier of D ;
set f = the Morphism of C;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: dom the Source of D = the carrier' of D by FUNCT_2:def 1;
A4: dom the Target of D = the carrier' of D by FUNCT_2:def 1;
defpred S1[ set ] means ( rng F c= $1 & ex E being Subcategory of D st
( the carrier of E = O & the carrier' of E = $1 ) );
consider MM being set such that
A5: for x being set holds
( x in MM iff ( x in bool the carrier' of D & S1[x] ) ) from XFAMILY:sch 1();
 set HH = { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } ;
reconsider M0 = union { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } as non empty Subset of the carrier' of D by CAT_2:19;
reconsider D0 = the Source of D | M0, C0 = the Target of D | M0 as Function of M0,O by CAT_2:20;
reconsider CC = the Comp of D || M0 as PartFunc of [:M0,M0:],M0 by CAT_2:20;
CatStr(# O,M0,D0,C0,CC #) is full Subcategory of D by CAT_2:21;
then A6: CatStr(# O,M0,D0,C0,CC #) is Subcategory of D ;
rng F c= M0
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in M0 )
assume y in rng F ; :: thesis: y in M0
then consider x being object such that
A7: x in dom F and
A8: y = F . x by FUNCT_1:def 3;
reconsider x = x as Morphism of C by A7;
A9: (Obj F) . (dom x) in O by A1, FUNCT_1:def 3;
A10: (Obj F) . (cod x) in O by A1, FUNCT_1:def 3;
A11: dom (F . x) in O by A9, CAT_1:69;
A12: cod (F . x) in O by A10, CAT_1:69;
A13: y in Hom ((dom (F . x)),(cod (F . x))) by A8;
Hom ((dom (F . x)),(cod (F . x))) in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by A11, A12;
hence y in M0 by A13, TARSKI:def 4; :: thesis: verum
end;
then A14: M0 in MM by A5, A6;
set M = meet MM;
A15: for Z being set st Z in MM holds
rng F c= Z by A5;
now :: thesis: for X being set st X in MM holds
F . the Morphism of C in X
let X be set ; :: thesis: ( X in MM implies F . the Morphism of C in X )
assume X in MM ; :: thesis: F . the Morphism of C in X
then A16: rng F c= X by A5;
F . the Morphism of C in rng F by A2, FUNCT_1:def 3;
hence F . the Morphism of C in X by A16; :: thesis: verum
end;
then reconsider M = meet MM as non empty set by A14, SETFAM_1:def 1;
M c= the carrier' of D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in the carrier' of D )
assume x in M ; :: thesis: x in the carrier' of D
then x in M0 by A14, SETFAM_1:def 1;
hence x in the carrier' of D ; :: thesis: verum
end;
then reconsider M = M as non empty Subset of the carrier' of D ;
set DOM = the Source of D | M;
set COD = the Target of D | M;
set COMP = the Comp of D || M;
A17: dom ( the Source of D | M) = M by A3, RELAT_1:62;
rng ( the Source of D | M) c= O
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Source of D | M) or y in O )
assume y in rng ( the Source of D | M) ; :: thesis: y in O
then consider x being object such that
A18: x in M and
A19: y = ( the Source of D | M) . x by A17, FUNCT_1:def 3;
reconsider x = x as Morphism of D by A18;
x in M0 by A14, A18, SETFAM_1:def 1;
then consider X being set such that
A20: x in X and
A21: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def 4;
consider a, b being Object of D such that
A22: X = Hom (a,b) and
A23: a in O and
b in O by A21;
dom x = a by A20, A22, CAT_1:1;
hence y in O by A17, A18, A19, A23, FUNCT_1:47; :: thesis: verum
end;
then reconsider DOM = the Source of D | M as Function of M,O by A17, FUNCT_2:def 1, RELSET_1:4;
A24: dom ( the Target of D | M) = M by A4, RELAT_1:62;
rng ( the Target of D | M) c= O
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Target of D | M) or y in O )
assume y in rng ( the Target of D | M) ; :: thesis: y in O
then consider x being object such that
A25: x in M and
A26: y = ( the Target of D | M) . x by A24, FUNCT_1:def 3;
reconsider x = x as Morphism of D by A25;
x in M0 by A14, A25, SETFAM_1:def 1;
then consider X being set such that
A27: x in X and
A28: X in { (Hom (a0,b)) where a0, b is Object of D : ( a0 in O & b in O ) } by TARSKI:def 4;
consider a, b being Object of D such that
A29: X = Hom (a,b) and
a in O and
A30: b in O by A28;
cod x = b by A27, A29, CAT_1:1;
hence y in O by A24, A25, A26, A30, FUNCT_1:47; :: thesis: verum
end;
then reconsider COD = the Target of D | M as Function of M,O by A24, FUNCT_2:def 1, RELSET_1:4;
A31: dom ( the Comp of D || M) c= [:M,M:] by RELAT_1:58;
rng ( the Comp of D || M) c= M
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ( the Comp of D || M) or y in M )
assume y in rng ( the Comp of D || M) ; :: thesis: y in M
then consider x being object such that
A32: x in dom ( the Comp of D || M) and
A33: y = ( the Comp of D || M) . x by FUNCT_1:def 3;
reconsider x1 = x `1 , x2 = x `2 as Element of M by A31, A32, MCART_1:10;
A34: x = [x1,x2] by A31, A32, MCART_1:21;
now :: thesis: for X being set st X in MM holds
y in X
let X be set ; :: thesis: ( X in MM implies y in X )
assume A35: X in MM ; :: thesis: y in X
then consider E being Subcategory of D such that
the carrier of E = O and
A36: the carrier' of E = X by A5;
reconsider y1 = x1, y2 = x2 as Morphism of E by A35, A36, SETFAM_1:def 1;
dom ( the Comp of D || M) = (dom the Comp of D) /\ [:M,M:] by RELAT_1:61;
then x in dom the Comp of D by A32, XBOOLE_0:def 4;
then A37: dom x1 = cod x2 by A34, CAT_1:15;
A38: dom y1 = dom x1 by CAT_2:9;
cod y2 = cod x2 by CAT_2:9;
then A39: x in dom the Comp of E by A34, A37, A38, CAT_1:15;
the Comp of E c= the Comp of D by CAT_2:def 4;
then the Comp of E . x = the Comp of D . x by A39, GRFUNC_1:2
.= y by A32, A33, FUNCT_1:47 ;
then y in rng the Comp of E by A39, FUNCT_1:def 3;
hence y in X by A36; :: thesis: verum
end;
hence y in M by A14, SETFAM_1:def 1; :: thesis: verum
end;
then reconsider COMP = the Comp of D || M as PartFunc of [:M,M:],M by A31, RELSET_1:4;
for o being Element of D st o in O holds
id o in M
proof
let o be Element of D; :: thesis: ( o in O implies id o in M )
assume A40: o in O ; :: thesis: id o in M
for X being set st X in MM holds
id o in X
proof
let X be set ; :: thesis: ( X in MM implies id o in X )
assume X in MM ; :: thesis: id o in X
then S1[X] by A5;
then consider E being Subcategory of D such that
A41: the carrier of E = O and
A42: the carrier' of E = X ;
o in the carrier of E by A40, A41;
then reconsider oo = o as Element of E ;
id oo = id o by CAT_2:def 4;
hence id o in X by A42; :: thesis: verum
end;
hence id o in M by A14, SETFAM_1:def 1; :: thesis: verum
end;
then reconsider T = CatStr(# O,M,DOM,COD,COMP #) as strict Subcategory of D by NATTRA_1:9;
take T ; :: thesis: ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T & ( for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
T is Subcategory of E ) )
thus ( the carrier of T = rng (Obj F) & rng F c= the carrier' of T ) by A14, A15, SETFAM_1:5; :: thesis: for E being Subcategory of D st the carrier of E = rng (Obj F) & rng F c= the carrier' of E holds
T is Subcategory of E
let E be Subcategory of D; :: thesis: ( the carrier of E = rng (Obj F) & rng F c= the carrier' of E implies T is Subcategory of E )
assume that
A43: the carrier of E = rng (Obj F) and
A44: rng F c= the carrier' of E ; :: thesis: T is Subcategory of E
thus the carrier of T c= the carrier of E by A43; :: according to CAT_2:def 4 :: thesis: ( ( for b1, b2 being Element of the carrier of T
for b3, b4 being Element of the carrier of E holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of T c= the Comp of E & ( for b1 being Element of the carrier of T
for b2 being Element of the carrier of E holds
( not b1 = b2 or id b1 = id b2 ) ) )
the carrier' of E c= the carrier' of D by CAT_2:7;
then the carrier' of E in MM by A5, A43, A44;
then A45: M c= the carrier' of E by SETFAM_1:3;
hereby :: thesis: ( the Comp of T c= the Comp of E & ( for b1 being Element of the carrier of T
for b2 being Element of the carrier of E holds
( not b1 = b2 or id b1 = id b2 ) ) )
let a, b be Object of T; :: thesis: for a9, b9 being Object of E st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
let a9, b9 be Object of E; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A46: a = a9 and
A47: b = b9 ; :: thesis: Hom (a,b) c= Hom (a9,b9)
thus Hom (a,b) c= Hom (a9,b9) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume x in Hom (a,b) ; :: thesis: x in Hom (a9,b9)
then consider f being Morphism of T such that
A48: x = f and
A49: dom f = a and
A50: cod f = b ;
reconsider g = f as Morphism of D by TARSKI:def 3;
reconsider f = f as Morphism of E by A45;
A51: dom g = a by A49, CAT_2:9;
A52: cod g = b by A50, CAT_2:9;
A53: a9 = dom f by A46, A51, CAT_2:9;
b9 = cod f by A47, A52, CAT_2:9;
hence x in Hom (a9,b9) by A48, A53; :: thesis: verum
end;
end;
A54: dom the Comp of T c= dom the Comp of E
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom the Comp of T or x in dom the Comp of E )
assume A55: x in dom the Comp of T ; :: thesis: x in dom the Comp of E
then reconsider x1 = x `1 , x2 = x `2 as Element of M by MCART_1:10;
reconsider y1 = x1, y2 = x2 as Morphism of T ;
reconsider z1 = x1, z2 = x2 as Morphism of E by A45;
A56: x = [x1,x2] by A55, MCART_1:21;
then A57: dom y1 = cod y2 by A55, CAT_1:15;
A58: dom y1 = dom x1 by CAT_2:9;
A59: dom z1 = dom x1 by CAT_2:9;
A60: cod y2 = cod x2 by CAT_2:9;
cod z2 = cod x2 by CAT_2:9;
hence x in dom the Comp of E by A56, A57, A58, A59, A60, CAT_1:15; :: thesis: verum
end;
now :: thesis: for x being object st x in dom the Comp of T holds
the Comp of T . x = the Comp of E . x
let x be object ; :: thesis: ( x in dom the Comp of T implies the Comp of T . x = the Comp of E . x )
assume A61: x in dom the Comp of T ; :: thesis: the Comp of T . x = the Comp of E . x
A62: the Comp of T c= the Comp of D by CAT_2:def 4;
A63: the Comp of E c= the Comp of D by CAT_2:def 4;
thus the Comp of T . x = the Comp of D . x by A61, A62, GRFUNC_1:2
.= the Comp of E . x by A54, A61, A63, GRFUNC_1:2 ; :: thesis: verum
end;
hence the Comp of T c= the Comp of E by A54, GRFUNC_1:2; :: thesis: for b1 being Element of the carrier of T
for b2 being Element of the carrier of E holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of T; :: thesis: for b1 being Element of the carrier of E holds
( not a = b1 or id a = id b1 )
let a9 be Object of E; :: thesis: ( not a = a9 or id a = id a9 )
reconsider b = a as Object of D by TARSKI:def 3;
assume A64: a = a9 ; :: thesis: id a = id a9
id a = id b by CAT_2:def 4;
hence id a = id a9 by A64, CAT_2:def 4; :: thesis: verum