Theorem estrcid

Description: The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020)

	Ref	Expression
Hypotheses	estrccat.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
	estrcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	estrcid.u	$$⊢\phi \to U\in V$$
	estrcid.x	$$⊢\phi \to X\in U$$
Assertion	estrcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$

Proof

Step	Hyp	Ref	Expression
1		estrccat.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
2		estrcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
3		estrcid.u	$$⊢\phi \to U\in V$$
4		estrcid.x	$$⊢\phi \to X\in U$$
5	1	estrccatid	$$⊢U\in V\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)\right)$$
6	3 5	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)\right)$$
7	6	simprd	$$⊢\phi \to \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)$$
8	2 7	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in U⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)$$
9		fveq2	$$⊢x=X\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
10	9	reseq2d	$$⊢x=X\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
11	10	adantl	$$⊢\left(\phi \wedge x=X\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
12		fvexd	$$⊢\phi \to {\mathrm{Base}}_X\in \mathrm{V}$$
13	12	resiexd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \mathrm{V}$$
14	8 11 4 13	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$