let A be Category; :: thesis: for a being Object of A holds 1Cat (a,(id a)) is Subcategory of A
let d be Object of A; :: thesis: 1Cat (d,(id d)) is Subcategory of A
thus the carrier of (1Cat (d,(id d))) c= the carrier of A :: according to CAT_2:def 4 :: thesis: ( ( 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 ) ) )
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of (1Cat (d,(id d))) or b in the carrier of A )
assume b in the carrier of (1Cat (d,(id d))) ; :: thesis: b in the carrier of A
then b = d by TARSKI:def 1;
hence b in the carrier of A ; :: thesis: verum
end;
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) :: thesis: ( 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))); :: thesis: 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; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) c= Hom (a9,b9) )
assume that
A1: a = a9 and
A2: b = b9 ; :: thesis: Hom (a,b) c= Hom (a9,b9)
A3: b9 = d by A2, TARSKI:def 1;
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 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; :: thesis: verum
end;
thus the Comp of (1Cat (d,(id d))) c= the Comp of A :: thesis: 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 x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Comp of (1Cat (d,(id d))) or x in the Comp of A )
assume x in the Comp of (1Cat (d,(id d))) ; :: thesis: x in the Comp of A
then x in {[[(id d),(id d)],(id d)]} by Th2;
then x = [[(id d),(id d)],(id d)] by TARSKI:def 1;
hence x in the Comp of A by Th1; :: thesis: verum
end;
let a be Object of (1Cat (d,(id d))); :: thesis: for b1 being Element of the carrier of A holds
( not a = b1 or id a = id b1 )
let a9 be Object of A; :: thesis: ( not a = a9 or id a = id a9 )
assume a = a9 ; :: thesis: id a = id a9
then a9 = d by TARSKI:def 1;
hence id a = id a9 by TARSKI:def 1; :: thesis: verum