let A be Category; for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A
let d be Object of A; 1Cat (d,(id d)) is Subcategory of A
thus
the carrier of (1Cat (d,(id d))) c= the carrier of A
CAT_2:def 4 ( ( for b1, b2 being Element of the carrier of (1Cat (d,(id d)))
for b3, b4 being Element of the carrier of A holds
( not b1 = b3 or not b2 = b4 or Hom (b1,b2) c= Hom (b3,b4) ) ) & the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )
thus
for a, b being Object of (1Cat (d,(id d)))
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)
( the Comp of (1Cat (d,(id d))) c= the Comp of A & ( for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 ) ) )proof
let a,
b be
Object of
(1Cat (d,(id d)));
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9)let a9,
b9 be
Object of
A;
( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that A1:
a = a9
and A2:
b = b9
;
Hom (a,b) c= Hom (a9,b9)
A3:
b9 = d
by A2, TARSKI:def 1;
let x be
object ;
TARSKI:def 3 ( not x in Hom (a,b) or x in Hom (a9,b9) )
assume
x in Hom (
a,
b)
;
x in Hom (a9,b9)
then A4:
x = id d
by TARSKI:def 1;
a9 = d
by A1, TARSKI:def 1;
hence
x in Hom (
a9,
b9)
by A3, A4, CAT_1:27;
verum
end;
thus
the Comp of (1Cat (d,(id d))) c= the Comp of A
for b1 being Element of the carrier of (1Cat (d,(id d)))
for b2 being Element of the carrier of A holds
( not b1 = b2 or id b1 = id b2 )
let a be Object of (1Cat (d,(id d))); for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )
let a9 be Object of A; ( not a = a9 or id a = id a9 )
assume
a = a9
; id a = id a9
then
a9 = d
by TARSKI:def 1;
hence
id a = id a9
by TARSKI:def 1; verum