let C be Category; :: thesis: ( C is quasi-discrete implies the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum } )

assume A1: C is quasi-discrete ; :: thesis: the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum }

set A = { (Hom (a,b)) where a, b is Element of C : verum } ;

set N = union { (Hom (a,b)) where a, b is Element of C : verum } ;

set B = { (Hom (a,a)) where a is Element of C : verum } ;

set M = union { (Hom (a,a)) where a is Element of C : verum } ;

A2: the carrier' of C = union { (Hom (a,b)) where a, b is Element of C : verum } by CAT_1:92;

thus the carrier' of C c= union { (Hom (a,a)) where a is Element of C : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (Hom (a,a)) where a is Element of C : verum } c= the carrier' of C

assume e in union { (Hom (a,a)) where a is Element of C : verum } ; :: thesis: e in the carrier' of C

then consider X being set such that

A6: e in X and

A7: X in { (Hom (a,a)) where a is Element of C : verum } by TARSKI:def 4;

ex a being Element of C st X = Hom (a,a) by A7;

hence e in the carrier' of C by A6; :: thesis: verum

assume A1: C is quasi-discrete ; :: thesis: the carrier' of C = union { (Hom (a,a)) where a is Element of C : verum }

set A = { (Hom (a,b)) where a, b is Element of C : verum } ;

set N = union { (Hom (a,b)) where a, b is Element of C : verum } ;

set B = { (Hom (a,a)) where a is Element of C : verum } ;

set M = union { (Hom (a,a)) where a is Element of C : verum } ;

A2: the carrier' of C = union { (Hom (a,b)) where a, b is Element of C : verum } by CAT_1:92;

thus the carrier' of C c= union { (Hom (a,a)) where a is Element of C : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (Hom (a,a)) where a is Element of C : verum } c= the carrier' of C

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (Hom (a,a)) where a is Element of C : verum } or e in the carrier' of C )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the carrier' of C or e in union { (Hom (a,a)) where a is Element of C : verum } )

assume e in the carrier' of C ; :: thesis: e in union { (Hom (a,a)) where a is Element of C : verum }

then consider X being set such that

A3: e in X and

A4: X in { (Hom (a,b)) where a, b is Element of C : verum } by A2, TARSKI:def 4;

consider a, b being Element of C such that

A5: X = Hom (a,b) by A4;

a = b by A1, A3, A5;

then X in { (Hom (a,a)) where a is Element of C : verum } by A5;

hence e in union { (Hom (a,a)) where a is Element of C : verum } by A3, TARSKI:def 4; :: thesis: verum

end;assume e in the carrier' of C ; :: thesis: e in union { (Hom (a,a)) where a is Element of C : verum }

then consider X being set such that

A3: e in X and

A4: X in { (Hom (a,b)) where a, b is Element of C : verum } by A2, TARSKI:def 4;

consider a, b being Element of C such that

A5: X = Hom (a,b) by A4;

a = b by A1, A3, A5;

then X in { (Hom (a,a)) where a is Element of C : verum } by A5;

hence e in union { (Hom (a,a)) where a is Element of C : verum } by A3, TARSKI:def 4; :: thesis: verum

assume e in union { (Hom (a,a)) where a is Element of C : verum } ; :: thesis: e in the carrier' of C

then consider X being set such that

A6: e in X and

A7: X in { (Hom (a,a)) where a is Element of C : verum } by TARSKI:def 4;

ex a being Element of C st X = Hom (a,a) by A7;

hence e in the carrier' of C by A6; :: thesis: verum