Theorem funcestrcsetclem5

Description: Lemma 5 for funcestrcsetc . (Contributed by AV, 23-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)$$
	funcestrcsetc.m	$$⊢M={\mathrm{Base}}_X$$
	funcestrcsetc.n	$$⊢N={\mathrm{Base}}_Y$$
Assertion	funcestrcsetclem5	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to XGY={\mathrm{I}\upharpoonright }_{\left(N^M\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		funcestrcsetc.m	$$⊢M={\mathrm{Base}}_X$$
9		funcestrcsetc.n	$$⊢N={\mathrm{Base}}_Y$$
10	7	adantr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
11		fveq2	$$⊢y=Y\to {\mathrm{Base}}_y={\mathrm{Base}}_Y$$
12		fveq2	$$⊢x=X\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
13	11 12	oveqan12rd	$$⊢\left(x=X\wedge y=Y\right)\to {{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
14	9 8	oveq12i	$$⊢N^M={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
15	13 14	eqtr4di	$$⊢\left(x=X\wedge y=Y\right)\to {{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}=N^M$$
16	15	reseq2d	$$⊢\left(x=X\wedge y=Y\right)\to {\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}={\mathrm{I}\upharpoonright }_{\left(N^M\right)}$$
17	16	adantl	$$⊢\left(\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\wedge \left(x=X\wedge y=Y\right)\right)\to {\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}={\mathrm{I}\upharpoonright }_{\left(N^M\right)}$$
18		simprl	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X\in B$$
19		simprr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to Y\in B$$
20		ovexd	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to N^M\in \mathrm{V}$$
21	20	resiexd	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to {\mathrm{I}\upharpoonright }_{\left(N^M\right)}\in \mathrm{V}$$
22	10 17 18 19 21	ovmpod	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to XGY={\mathrm{I}\upharpoonright }_{\left(N^M\right)}$$