Theorem 1strwunbndx

Description: A constructed one-slot structure in a weak universe containing the index of the base set extractor. (Contributed by AV, 27-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		1str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
2		1strwun.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
3		1strwunbndx.b	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ 𝑈 )
4	2	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝑈 ∈ WUni )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → ( Base ‘ ndx ) ∈ 𝑈 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝐵 ∈ 𝑈 )
7	4 5 6	wunop	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ ∈ 𝑈 )
8	4 7	wunsn	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ∈ 𝑈 )
9	1 8	eqeltrid	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑈 ) → 𝐺 ∈ 𝑈 )