Metamath Proof Explorer


Theorem catcccocl

Description: The composition operation 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 catcccocl
|- ( ph -> ( comp ` 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 ccoid
 |-  comp = Slot ( comp ` ndx )
6 1 2 3 4 5 catcslotelcl
 |-  ( ph -> ( comp ` X ) e. U )