Theorem catcbascl

Description: 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	catcbascl	$$⊢\phi \to 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	1 2 3	catcbas	$$⊢\phi \to B=U\cap \mathrm{Cat}$$
6	4 5	eleqtrd	$$⊢\phi \to X\in \left(U\cap \mathrm{Cat}\right)$$
7	6	elin1d	$$⊢\phi \to X\in U$$