Theorem basndxelwund

Description: The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun . (Contributed by AV, 27-Mar-2020) (Revised by AV, 17-Oct-2024)

	Ref	Expression
Hypotheses	basndxelwund.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	basndxelwund.o	$$⊢\phi \to \mathrm{\omega }\in U$$
Assertion	basndxelwund	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$

Proof

Step	Hyp	Ref	Expression
1		basndxelwund.u	$$⊢\phi \to U\in \mathrm{WUni}$$
2		basndxelwund.o	$$⊢\phi \to \mathrm{\omega }\in U$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4	1 2	wunndx	$$⊢\phi \to \mathrm{ndx}\in U$$
5	3 1 4	wunstr	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$