Metamath Proof Explorer


Theorem catcbaselcl

Description: The base 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 φ U WUni
catcbascl.x φ X B
Assertion catcbaselcl φ Base X U

Proof

Step Hyp Ref Expression
1 catcbascl.c C = CatCat U
2 catcbascl.b B = Base C
3 catcbascl.u φ U WUni
4 catcbascl.x φ X B
5 baseid Base = Slot Base ndx
6 1 2 3 4 5 catcslotelcl φ Base X U