A1:
the carrier' of (IdCat C) = { (id a) where a is Object of C : verum }
by Def20;
thus
IdCat C is quasi-discrete
NATTRA_1:def 20 IdCat C is pseudo-discrete
let c be Element of (IdCat C); NATTRA_1:def 19 Hom (c,c) is trivial
let x, y be object ; ZFMISC_1:def 10 ( 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) )
; 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; verum