Theorem funcestrcsetclem4

Description: Lemma 4 for funcestrcsetc . (Contributed by AV, 22-Mar-2020)

	Ref	Expression
Hypotheses	funcestrcsetc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
	funcestrcsetc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcestrcsetc.b	$$⊢B={\mathrm{Base}}_E$$
	funcestrcsetc.c	$$⊢C={\mathrm{Base}}_S$$
	funcestrcsetc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcestrcsetc.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
	funcestrcsetc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
Assertion	funcestrcsetclem4	$$⊢\phi \to GFn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
2		funcestrcsetc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
3		funcestrcsetc.b	$$⊢B={\mathrm{Base}}_E$$
4		funcestrcsetc.c	$$⊢C={\mathrm{Base}}_S$$
5		funcestrcsetc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
6		funcestrcsetc.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
7		funcestrcsetc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
8		eqid	$$⊢\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
9		ovex	$$⊢{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\in \mathrm{V}$$
10		resiexg	$$⊢{{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\in \mathrm{V}$$
11	9 10	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\in \mathrm{V}$$
12	8 11	fnmpoi	$$⊢\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)Fn\left(B\times B\right)$$
13	7	fneq1d	$$⊢\phi \to \left(GFn\left(B\times B\right)\leftrightarrow \left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)Fn\left(B\times B\right)\right)$$
14	12 13	mpbiri	$$⊢\phi \to GFn\left(B\times B\right)$$