Theorem catcslotelcl

Description: A slot entry 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$$
	catcslotelcl.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
Assertion	catcslotelcl	$$⊢\phi \to E\left(X\right)\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		catcslotelcl.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
6	1 2 3 4	catcbascl	$$⊢\phi \to X\in U$$
7	5 3 6	wunstr	$$⊢\phi \to E\left(X\right)\in U$$