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	|- ( ph -> U e. WUni )
	basndxelwund.o	|- ( ph -> _om e. U )
Assertion	basndxelwund	|- ( ph -> ( Base ` ndx ) e. U )

Proof

Step	Hyp	Ref	Expression
1		basndxelwund.u	|- ( ph -> U e. WUni )
2		basndxelwund.o	|- ( ph -> _om e. U )
3		baseid	|- Base = Slot ( Base ` ndx )
4	1 2	wunndx	|- ( ph -> ndx e. U )
5	3 1 4	wunstr	|- ( ph -> ( Base ` ndx ) e. U )