Theorem setc1strwun

Description: A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020)

	Ref	Expression
Hypotheses	setc1strwun.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	setc1strwun.c	$$⊢C={\mathrm{Base}}_S$$
	setc1strwun.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	setc1strwun.o	$$⊢\phi \to \mathrm{\omega }\in U$$
Assertion	setc1strwun	$$⊢\left(\phi \wedge X\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in U$$

Proof

Step	Hyp	Ref	Expression
1		setc1strwun.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
2		setc1strwun.c	$$⊢C={\mathrm{Base}}_S$$
3		setc1strwun.u	$$⊢\phi \to U\in \mathrm{WUni}$$
4		setc1strwun.o	$$⊢\phi \to \mathrm{\omega }\in U$$
5	1 3	setcbas	$$⊢\phi \to U={\mathrm{Base}}_S$$
6	2 5	eqtr4id	$$⊢\phi \to C=U$$
7	6	eleq2d	$$⊢\phi \to \left(X\in C\leftrightarrow X\in U\right)$$
8	7	biimpa	$$⊢\left(\phi \wedge X\in C\right)\to X\in U$$
9		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
10	9 3 4	1strwun	$$⊢\left(\phi \wedge X\in U\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in U$$
11	8 10	syldan	$$⊢\left(\phi \wedge X\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in U$$