let C be Category; the carrier' of C = union { (Hom (a,b)) where a, b is Object of C : verum }
set A = { (Hom (a,b)) where a, b is Object of C : verum } ;
set M = union { (Hom (a,b)) where a, b is Object of C : verum } ;
thus
the carrier' of C c= union { (Hom (a,b)) where a, b is Object of C : verum }
XBOOLE_0:def 10 union { (Hom (a,b)) where a, b is Object of C : verum } c= the carrier' of Cproof
let e be
object ;
TARSKI:def 3 ( not e in the carrier' of C or e in union { (Hom (a,b)) where a, b is Object of C : verum } )
assume
e in the
carrier' of
C
;
e in union { (Hom (a,b)) where a, b is Object of C : verum }
then reconsider e =
e as
Morphism of
C ;
A1:
e in Hom (
(dom e),
(cod e))
;
Hom (
(dom e),
(cod e))
in { (Hom (a,b)) where a, b is Object of C : verum }
;
hence
e in union { (Hom (a,b)) where a, b is Object of C : verum }
by A1, TARSKI:def 4;
verum
end;
let e be object ; TARSKI:def 3 ( not e in union { (Hom (a,b)) where a, b is Object of C : verum } or e in the carrier' of C )
assume
e in union { (Hom (a,b)) where a, b is Object of C : verum }
; e in the carrier' of C
then consider X being set such that
A2:
e in X
and
A3:
X in { (Hom (a,b)) where a, b is Object of C : verum }
by TARSKI:def 4;
ex a, b being Object of C st X = Hom (a,b)
by A3;
hence
e in the carrier' of C
by A2; verum