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 ⊢ G = Base ndx B
1strwun.u ⊢ φ → U ∈ WUni
1strwun.o ⊢ φ → ω ∈ U
Assertion 1strwun ⊢ φ ∧ B ∈ U → G ∈ U

Proof

Step Hyp Ref Expression
1 1str.g ⊢ G = Base ndx B
2 1strwun.u ⊢ φ → U ∈ WUni
3 1strwun.o ⊢ φ → ω ∈ U
4 2 3 basndxelwund ⊢ φ → Base ndx ∈ U
5 1 2 4 1strwunbndx ⊢ φ ∧ B ∈ U → G ∈ U