A1: the carrier' of (IdCat C) = { (id a) where a is Object of C : verum } by Def20;
thus IdCat C is quasi-discrete :: according to NATTRA_1:def 20 :: thesis: IdCat C is pseudo-discrete
proof
let a, b be Element of (IdCat C); :: according to NATTRA_1:def 18 :: thesis: ( Hom (a,b) <> {} implies a = b )
assume Hom (a,b) <> {} ; :: thesis: a = b
then consider m being object such that
A2: m in Hom (a,b) by XBOOLE_0:def 1;
reconsider m = m as Morphism of (IdCat C) by A2;
m in the carrier' of (IdCat C) ;
then consider cc being Element of C such that
A3: m = id cc by A1;
reconsider c = cc as Element of (IdCat C) by Def20;
A4: id c in Hom (a,b) by A3, A2, CAT_2:def 4;
hence a = dom (id c) by CAT_1:1
.= cod (id c)
.= b by A4, CAT_1:1 ;
:: thesis: verum
end;
let c be Element of (IdCat C); :: according to NATTRA_1:def 19 :: thesis: Hom (c,c) is trivial
let x, y be object ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in Hom (c,c) or not y in Hom (c,c) or x = y )
assume A5: ( x in Hom (c,c) & y in Hom (c,c) ) ; :: thesis: x = y
then reconsider a = x, b = y as Morphism of (IdCat C) ;
set M = { (id o) where o is Object of C : verum } ;
a in the carrier' of (IdCat C) ;
then a in { (id o) where o is Object of C : verum } by Def20;
then consider ox being Element of C such that
A6: a = id ox ;
b in the carrier' of (IdCat C) ;
then b in { (id o) where o is Object of C : verum } by Def20;
then consider oy being Element of C such that
A7: b = id oy ;
reconsider cc = c as Element of C by Def20;
A8: Hom (c,c) c= Hom (cc,cc) by CAT_2:def 4;
ox = dom (id ox)
.= cc by A8, A5, A6, CAT_1:1
.= dom (id oy) by A8, A5, A7, CAT_1:1
.= oy ;
hence x = y by A6, A7; :: thesis: verum