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	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
	1strwun.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	1strwunbndx.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
Assertion	1strwunbndx	$$⊢\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		1strwunbndx.b	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
4	2	adantr	$$⊢\left(\phi \wedge B\in U\right)\to U\in \mathrm{WUni}$$
5	3	adantr	$$⊢\left(\phi \wedge B\in U\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
6		simpr	$$⊢\left(\phi \wedge B\in U\right)\to B\in U$$
7	4 5 6	wunop	$$⊢\left(\phi \wedge B\in U\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\in U$$
8	4 7	wunsn	$$⊢\left(\phi \wedge B\in U\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\in U$$
9	1 8	eqeltrid	$$⊢\left(\phi \wedge B\in U\right)\to G\in U$$