Theorem funcsetcestrclem7

Description: Lemma 7 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)$$
	funcsetcestrc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
Assertion	funcsetcestrclem7	$$⊢\left(\phi \wedge X\in C\right)\to \left(XGX\right)\left(\mathrm{Id}\left(S\right)\left(X\right)\right)=\mathrm{Id}\left(E\right)\left(F\left(X\right)\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		funcsetcestrc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
8	1 2 3 4 5 6	funcsetcestrclem5	$$⊢\left(\phi \wedge \left(X\in C\wedge X\in C\right)\right)\to XGX={\mathrm{I}\upharpoonright }_{\left(X^X\right)}$$
9	8	anabsan2	$$⊢\left(\phi \wedge X\in C\right)\to XGX={\mathrm{I}\upharpoonright }_{\left(X^X\right)}$$
10		eqid	$$⊢\mathrm{Id}\left(S\right)=\mathrm{Id}\left(S\right)$$
11	4	adantr	$$⊢\left(\phi \wedge X\in C\right)\to U\in \mathrm{WUni}$$
12	1 4	setcbas	$$⊢\phi \to U={\mathrm{Base}}_S$$
13	2 12	eqtr4id	$$⊢\phi \to C=U$$
14	13	eleq2d	$$⊢\phi \to \left(X\in C\leftrightarrow X\in U\right)$$
15	14	biimpa	$$⊢\left(\phi \wedge X\in C\right)\to X\in U$$
16	1 10 11 15	setcid	$$⊢\left(\phi \wedge X\in C\right)\to \mathrm{Id}\left(S\right)\left(X\right)={\mathrm{I}\upharpoonright }_X$$
17	9 16	fveq12d	$$⊢\left(\phi \wedge X\in C\right)\to \left(XGX\right)\left(\mathrm{Id}\left(S\right)\left(X\right)\right)=\left({\mathrm{I}\upharpoonright }_{\left(X^X\right)}\right)\left({\mathrm{I}\upharpoonright }_X\right)$$
18		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X$$
19		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X\underset{1-1\; onto}{⟶}X\to \left({\mathrm{I}\upharpoonright }_X\right):X⟶X$$
20	18 19	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_X\right):X⟶X$$
21		simpr	$$⊢\left(\phi \wedge X\in C\right)\to X\in C$$
22	21 21	elmapd	$$⊢\left(\phi \wedge X\in C\right)\to \left({\mathrm{I}\upharpoonright }_X\in \left(X^X\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_X\right):X⟶X\right)$$
23	20 22	mpbiri	$$⊢\left(\phi \wedge X\in C\right)\to {\mathrm{I}\upharpoonright }_X\in \left(X^X\right)$$
24		fvresi	$$⊢{\mathrm{I}\upharpoonright }_X\in \left(X^X\right)\to \left({\mathrm{I}\upharpoonright }_{\left(X^X\right)}\right)\left({\mathrm{I}\upharpoonright }_X\right)={\mathrm{I}\upharpoonright }_X$$
25	23 24	syl	$$⊢\left(\phi \wedge X\in C\right)\to \left({\mathrm{I}\upharpoonright }_{\left(X^X\right)}\right)\left({\mathrm{I}\upharpoonright }_X\right)={\mathrm{I}\upharpoonright }_X$$
26		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
27	26	1strbas	$$⊢X\in C\to X={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}$$
28	21 27	syl	$$⊢\left(\phi \wedge X\in C\right)\to X={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}$$
29	28	reseq2d	$$⊢\left(\phi \wedge X\in C\right)\to {\mathrm{I}\upharpoonright }_X={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}}$$
30	25 29	eqtrd	$$⊢\left(\phi \wedge X\in C\right)\to \left({\mathrm{I}\upharpoonright }_{\left(X^X\right)}\right)\left({\mathrm{I}\upharpoonright }_X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}}$$
31	1 2 3	funcsetcestrclem1	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
32	31	fveq2d	$$⊢\left(\phi \wedge X\in C\right)\to \mathrm{Id}\left(E\right)\left(F\left(X\right)\right)=\mathrm{Id}\left(E\right)\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\right)$$
33		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
34	1 2 4 5	setc1strwun	$$⊢\left(\phi \wedge X\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in U$$
35	7 33 11 34	estrcid	$$⊢\left(\phi \wedge X\in C\right)\to \mathrm{Id}\left(E\right)\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}}$$
36	32 35	eqtr2d	$$⊢\left(\phi \wedge X\in C\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}}}=\mathrm{Id}\left(E\right)\left(F\left(X\right)\right)$$
37	17 30 36	3eqtrd	$$⊢\left(\phi \wedge X\in C\right)\to \left(XGX\right)\left(\mathrm{Id}\left(S\right)\left(X\right)\right)=\mathrm{Id}\left(E\right)\left(F\left(X\right)\right)$$