Theorem rngcidALTV

Description: The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngccatALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
	rngcidALTV.b	$$⊢B={\mathrm{Base}}_C$$
	rngcidALTV.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	rngcidALTV.u	$$⊢\phi \to U\in V$$
	rngcidALTV.x	$$⊢\phi \to X\in B$$
	rngcidALTV.s	$$⊢S={\mathrm{Base}}_X$$
Assertion	rngcidALTV	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_S$$

Proof

Step	Hyp	Ref	Expression
1		rngccatALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
2		rngcidALTV.b	$$⊢B={\mathrm{Base}}_C$$
3		rngcidALTV.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
4		rngcidALTV.u	$$⊢\phi \to U\in V$$
5		rngcidALTV.x	$$⊢\phi \to X\in B$$
6		rngcidALTV.s	$$⊢S={\mathrm{Base}}_X$$
7	1 2	rngccatidALTV	$$⊢U\in V\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in B⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)\right)$$
8	4 7	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in B⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)\right)$$
9	8	simprd	$$⊢\phi \to \mathrm{Id}\left(C\right)=\left(x\in B⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)$$
10	3 9	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in B⟼{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\right)$$
11		fveq2	$$⊢x=X\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
12	11	adantl	$$⊢\left(\phi \wedge x=X\right)\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
13	12	reseq2d	$$⊢\left(\phi \wedge x=X\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
14		fvex	$$⊢{\mathrm{Base}}_X\in \mathrm{V}$$
15		resiexg	$$⊢{\mathrm{Base}}_X\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \mathrm{V}$$
16	14 15	mp1i	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \mathrm{V}$$
17	10 13 5 16	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
18	6	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_S={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
19	17 18	syl6eqr	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_S$$