This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to U \in WUni$
	basndxelwund.o	$⊢ φ \to ω \in U$
Assertion	basndxelwund	$⊢ φ \to {Base}_{ndx} \in U$

Proof

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