Theorem funcestrcsetclem7

Description: Lemma 7 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)$$
Assertion	funcestrcsetclem7	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(E\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\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	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_X$$
9	1 2 3 4 5 6 7 8 8	funcestrcsetclem5	$$⊢\left(\phi \wedge \left(X\in B\wedge X\in B\right)\right)\to XGX={\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)}$$
10	9	anabsan2	$$⊢\left(\phi \wedge X\in B\right)\to XGX={\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)}$$
11		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
12	5	adantr	$$⊢\left(\phi \wedge X\in B\right)\to U\in \mathrm{WUni}$$
13	1 5	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_E$$
14	3 13	eqtr4id	$$⊢\phi \to B=U$$
15	14	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in U\right)$$
16	15	biimpa	$$⊢\left(\phi \wedge X\in B\right)\to X\in U$$
17	1 11 12 16	estrcid	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(E\right)\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
18	10 17	fveq12d	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(E\right)\left(X\right)\right)=\left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)$$
19		fvex	$$⊢{\mathrm{Base}}_X\in \mathrm{V}$$
20	19 19	pm3.2i	$$⊢\left({\mathrm{Base}}_X\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)$$
21	20	a1i	$$⊢\left(\phi \wedge X\in B\right)\to \left({\mathrm{Base}}_X\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)$$
22		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right):{\mathrm{Base}}_X\underset{1-1\; onto}{⟶}{\mathrm{Base}}_X$$
23		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right):{\mathrm{Base}}_X\underset{1-1\; onto}{⟶}{\mathrm{Base}}_X\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right):{\mathrm{Base}}_X⟶{\mathrm{Base}}_X$$
24	22 23	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right):{\mathrm{Base}}_X⟶{\mathrm{Base}}_X$$
25		elmapg	$$⊢\left({\mathrm{Base}}_X\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right):{\mathrm{Base}}_X⟶{\mathrm{Base}}_X\right)$$
26	24 25	mpbiri	$$⊢\left({\mathrm{Base}}_X\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)$$
27		fvresi	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)\to \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
28	21 26 27	3syl	$$⊢\left(\phi \wedge X\in B\right)\to \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_X}^{{\mathrm{Base}}_X}\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
29	1 2 3 4 5 6	funcestrcsetclem1	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$
30	29	fveq2d	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(S\right)\left(F\left(X\right)\right)=\mathrm{Id}\left(S\right)\left({\mathrm{Base}}_X\right)$$
31		eqid	$$⊢\mathrm{Id}\left(S\right)=\mathrm{Id}\left(S\right)$$
32	1 3 5	estrcbasbas	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{Base}}_X\in U$$
33	2 31 12 32	setcid	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(S\right)\left({\mathrm{Base}}_X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
34	30 33	eqtr2d	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$
35	18 28 34	3eqtrd	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(E\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$