Theorem funcsetcestrclem3

Description: Lemma 3 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$$
	funcsetcestrclem3.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
	funcsetcestrclem3.b	$$⊢B={\mathrm{Base}}_E$$
Assertion	funcsetcestrclem3	$$⊢\phi \to F:C⟶B$$

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		funcsetcestrclem3.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
7		funcsetcestrclem3.b	$$⊢B={\mathrm{Base}}_E$$
8	1 2 4 5	setc1strwun	$$⊢\left(\phi \wedge x\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\in U$$
9	6 4	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_E$$
10	9	eqcomd	$$⊢\phi \to {\mathrm{Base}}_E=U$$
11	10	adantr	$$⊢\left(\phi \wedge x\in C\right)\to {\mathrm{Base}}_E=U$$
12	8 11	eleqtrrd	$$⊢\left(\phi \wedge x\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\in {\mathrm{Base}}_E$$
13	12 7	eleqtrrdi	$$⊢\left(\phi \wedge x\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\in B$$
14	3 13	fmpt3d	$$⊢\phi \to F:C⟶B$$