defpred S1[ Object of C] means verum;
deffunc H1( Object of C) -> Morphism of $1,$1 = id $1;
defpred S2[ Object of C] means H1($1) in the carrier' of C;
set M = { H1(a) where a is Object of C : S1[a] } ;
set N = { H1(a) where a is Object of C : S2[a] } ;
set N9 = { H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } ;
defpred S3[ Object of C] means ( H1($1) in the carrier' of C & S1[$1] );
set N99 = { H1(a) where a is Object of C : S3[a] } ;
set a = the Object of C;
A1:
id the Object of C in { H1(a) where a is Object of C : S1[a] }
;
A2:
for a being Object of C holds
( S2[a] iff S1[a] )
;
A3:
{ H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S1[a] }
from FRAENKEL:sch 3(A2);
A4:
for a being Object of C holds
( S2[a] iff S3[a] )
;
A5:
{ H1(a) where a is Object of C : S2[a] } = { H1(a) where a is Object of C : S3[a] }
from FRAENKEL:sch 3(A4);
{ H1(a) where a is Object of C : ( H1(a) in the carrier' of C & S1[a] ) } c= the carrier' of C
from FRAENKEL:sch 17();
then reconsider M = { H1(a) where a is Object of C : S1[a] } as non empty Subset of the carrier' of C by A3, A5, A1;
A6:
rng ( the Comp of C || M) c= M
proof
let x be
object ;
TARSKI:def 3 ( not x in rng ( the Comp of C || M) or x in M )
assume
x in rng ( the Comp of C || M)
;
x in M
then consider y being
object such that A7:
y in dom ( the Comp of C || M)
and A8:
x = ( the Comp of C || M) . y
by FUNCT_1:def 3;
A9:
y in (dom the Comp of C) /\ [:M,M:]
by A7, RELAT_1:61;
then A10:
y in dom the
Comp of
C
by XBOOLE_0:def 4;
y in [:M,M:]
by A9, XBOOLE_0:def 4;
then consider y1,
y2 being
object such that A11:
y1 in M
and A12:
y2 in M
and A13:
y = [y1,y2]
by ZFMISC_1:84;
consider a1 being
Object of
C such that A14:
y1 = id a1
by A11;
A15:
Hom (
a1,
a1)
<> {}
;
consider a2 being
Object of
C such that A16:
y2 = id a2
by A12;
A17:
a1 =
dom (id a1)
.=
cod (id a2)
by A13, A14, A16, A10, CAT_1:15
.=
a2
;
id a1 =
(id a1) * (id a1)
.=
(id a1) (*) (id a2)
by A15, A17, CAT_1:def 13
.=
the
Comp of
C . (
(id a1),
(id a2))
by A13, A14, A16, A10, CAT_1:def 1
.=
x
by A8, A9, A13, A14, A16, FUNCT_1:48
;
hence
x in M
;
verum
end;
the Comp of C || M is PartFunc of [:M,M:], the carrier' of C
by PARTFUN1:10;
then reconsider COMP = the Comp of C || M as PartFunc of [:M,M:],M by A6, RELSET_1:6;
A18:
the carrier of C c= the carrier of C
;
for o being Element of C st o in the carrier of C holds
id o in M
;
then reconsider A = CatStr(# the carrier of C,M,( the Source of C | M),( the Target of C | M),COMP #) as Subcategory of C by Th5, A18;
reconsider A = A as strict Subcategory of C ;
take
A
; ( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } )
thus
( the carrier of A = the carrier of C & the carrier' of A = { (id a) where a is Object of C : verum } )
; verum