let C be Category; :: thesis: for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

let O be non empty Subset of the carrier of C; :: thesis: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

set M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

A1: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C

let O be non empty Subset of the carrier of C; :: thesis: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C

set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

set M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;

A1: union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } or x in the carrier' of C )

assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: x in the carrier' of C

then consider X being set such that

A2: x in X and

A3: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;

ex a, b being Object of C st

( X = Hom (a,b) & a in O & b in O ) by A3;

hence x in the carrier' of C by A2; :: thesis: verum

end;assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: x in the carrier' of C

then consider X being set such that

A2: x in X and

A3: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;

ex a, b being Object of C st

( X = Hom (a,b) & a in O & b in O ) by A3;

hence x in the carrier' of C by A2; :: thesis: verum

now :: thesis: ex f being set st f in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }

hence
union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
by A1; :: thesis: verumset a = the Element of O;

reconsider a = the Element of O as Object of C ;

( id a in Hom (a,a) & Hom (a,a) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) by CAT_1:27;

then id a in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;

hence ex f being set st f in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: verum

end;reconsider a = the Element of O as Object of C ;

( id a in Hom (a,a) & Hom (a,a) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) by CAT_1:27;

then id a in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;

hence ex f being set st f in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: verum