Theorem 1strwun

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

	Ref	Expression
Hypotheses	1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
	1strwun.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	1strwun.o	$$⊢\phi \to \mathrm{\omega }\in U$$
Assertion	1strwun	$$⊢\left(\phi \wedge B\in U\right)\to G\in U$$

Proof

Step	Hyp	Ref	Expression
1		1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
2		1strwun.u	$$⊢\phi \to U\in \mathrm{WUni}$$
3		1strwun.o	$$⊢\phi \to \mathrm{\omega }\in U$$
4		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
5	2 3	wunndx	$$⊢\phi \to \mathrm{ndx}\in U$$
6	4 2 5	wunstr	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
7	1 2 6	1strwunbndx	$$⊢\left(\phi \wedge B\in U\right)\to G\in U$$