Theorem funcsetcestrclem4

Description: Lemma 4 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$$
	funcsetcestrc.g	$$⊢\phi \to G=\left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)$$
Assertion	funcsetcestrclem4	$$⊢\phi \to GFn\left(C\times C\right)$$

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		funcsetcestrc.g	$$⊢\phi \to G=\left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)$$
7		eqid	$$⊢\left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)=\left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)$$
8		ovex	$$⊢y^x\in \mathrm{V}$$
9		resiexg	$$⊢y^x\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{\left(y^x\right)}\in \mathrm{V}$$
10	8 9	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\in \mathrm{V}$$
11	7 10	fnmpoi	$$⊢\left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)Fn\left(C\times C\right)$$
12	6	fneq1d	$$⊢\phi \to \left(GFn\left(C\times C\right)\leftrightarrow \left(x\in C,y\in C⟼{\mathrm{I}\upharpoonright }_{\left(y^x\right)}\right)Fn\left(C\times C\right)\right)$$
13	11 12	mpbiri	$$⊢\phi \to GFn\left(C\times C\right)$$