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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	basndxelwund.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
Assertion	basndxelwund	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		basndxelwund.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		basndxelwund.o	⊢ ( 𝜑 → ω ∈ 𝑈 )
3		baseid	⊢ Base = Slot ( Base ‘ ndx )
4	1 2	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
5	3 1 4	wunstr	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )