Theorem funcsetcestrclem2

Description: Lemma 2 for funcsetcestrc . (Contributed by AV, 27-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		funcsetcestrc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
2		funcsetcestrc.c	$$⊢C={\mathrm{Base}}_S$$
3		funcsetcestrc.f	$$⊢\phi \to F=\left(x\in C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\right)$$
4		funcsetcestrc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
5		funcsetcestrc.o	$$⊢\phi \to \mathrm{\omega }\in U$$
6	1 2 3	funcsetcestrclem1	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
7	1 2 4 5	setc1strwun	$$⊢\left(\phi \wedge X\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in U$$
8	6 7	eqeltrd	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)\in U$$