Metamath Proof Explorer


Theorem catchomcl

Description: The Hom-set of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl . (Contributed by AV, 14-Oct-2024)

Ref Expression
Hypotheses catcbascl.c
|- C = ( CatCat ` U )
catcbascl.b
|- B = ( Base ` C )
catcbascl.u
|- ( ph -> U e. WUni )
catcbascl.x
|- ( ph -> X e. B )
Assertion catchomcl
|- ( ph -> ( Hom ` X ) e. U )

Proof

Step Hyp Ref Expression
1 catcbascl.c
 |-  C = ( CatCat ` U )
2 catcbascl.b
 |-  B = ( Base ` C )
3 catcbascl.u
 |-  ( ph -> U e. WUni )
4 catcbascl.x
 |-  ( ph -> X e. B )
5 homid
 |-  Hom = Slot ( Hom ` ndx )
6 1 2 3 4 5 catcslotelcl
 |-  ( ph -> ( Hom ` X ) e. U )