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

Metamath Proof Explorer

Theorem 1strwun

Description: A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020) (Proof shortened by AV, 17-Oct-2024)

Ref Expression
Hypotheses 1str.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
1strwun.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
1strwun.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
Assertion 1strwun ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝐺 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 1str.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
2 1strwun.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
3 1strwun.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
4 2 3 basndxelwund ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
5 1 2 4 1strwunbndx ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝐺 ∈ 𝑈 )