Theorem 1strwun

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

	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		df-base	⊢ Base = Slot 1
5	2 3	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )
6	4 2 5	wunstr	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
7	1 2 6	1strwunbndx	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝐺 ∈ 𝑈 )