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	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngcidALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	rngcidALTV.o	⊢ 1 = ( Id ‘ 𝐶 )
	rngcidALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcidALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	rngcidALTV.s	⊢ 𝑆 = ( Base ‘ 𝑋 )
Assertion	rngcidALTV	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		rngccatALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
2		rngcidALTV.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rngcidALTV.o	⊢ 1 = ( Id ‘ 𝐶 )
4		rngcidALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
5		rngcidALTV.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		rngcidALTV.s	⊢ 𝑆 = ( Base ‘ 𝑋 )
7	1 2	rngccatidALTV	⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
8	4 7	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
9	8	simprd	⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
10	3 9	eqtrid	⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
11		fveq2	⊢ ( 𝑥 = 𝑋 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
13	12	reseq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( I ↾ ( Base ‘ 𝑥 ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
14		fvex	⊢ ( Base ‘ 𝑋 ) ∈ V
15		resiexg	⊢ ( ( Base ‘ 𝑋 ) ∈ V → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ V )
16	14 15	mp1i	⊢ ( 𝜑 → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ V )
17	10 13 5 16	fvmptd	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
18	6	reseq2i	⊢ ( I ↾ 𝑆 ) = ( I ↾ ( Base ‘ 𝑋 ) )
19	17 18	eqtr4di	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( I ↾ 𝑆 ) )