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=\mathrm{CatCat}\left(U\right)$$
	catcbascl.b	$$⊢B={\mathrm{Base}}_C$$
	catcbascl.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	catcbascl.x	$$⊢\phi \to X\in B$$
Assertion	catcbaselcl	$$⊢\phi \to {\mathrm{Base}}_X\in U$$

Proof

Step	Hyp	Ref	Expression
1		catcbascl.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catcbascl.b	$$⊢B={\mathrm{Base}}_C$$
3		catcbascl.u	$$⊢\phi \to U\in \mathrm{WUni}$$
4		catcbascl.x	$$⊢\phi \to X\in B$$
5		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
6	1 2 3 4 5	catcslotelcl	$$⊢\phi \to {\mathrm{Base}}_X\in U$$