Theorem rngcrescrhm

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Hypotheses	rngcrescrhm.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcrescrhm.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	rngcrescrhm.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
	rngcrescrhm.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion	rngcrescrhm	⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s 𝑅 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		rngcrescrhm.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3		rngcrescrhm.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4		rngcrescrhm.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5		eqid	⊢ ( 𝐶 ↾cat 𝐻 ) = ( 𝐶 ↾cat 𝐻 )
6	2	fvexi	⊢ 𝐶 ∈ V
7	6	a1i	⊢ ( 𝜑 → 𝐶 ∈ V )
8		incom	⊢ ( Ring ∩ 𝑈 ) = ( 𝑈 ∩ Ring )
9	3 8	eqtrdi	⊢ ( 𝜑 → 𝑅 = ( 𝑈 ∩ Ring ) )
10		inex1g	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Ring ) ∈ V )
11	1 10	syl	⊢ ( 𝜑 → ( 𝑈 ∩ Ring ) ∈ V )
12	9 11	eqeltrd	⊢ ( 𝜑 → 𝑅 ∈ V )
13		inss1	⊢ ( Ring ∩ 𝑈 ) ⊆ Ring
14	3 13	eqsstrdi	⊢ ( 𝜑 → 𝑅 ⊆ Ring )
15		xpss12	⊢ ( ( 𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring ) → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
16	14 14 15	syl2anc	⊢ ( 𝜑 → ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) )
17		rhmfn	⊢ RingHom Fn ( Ring × Ring )
18		fnssresb	⊢ ( RingHom Fn ( Ring × Ring ) → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) ↔ ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) ) )
19	17 18	mp1i	⊢ ( 𝜑 → ( ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) ↔ ( 𝑅 × 𝑅 ) ⊆ ( Ring × Ring ) ) )
20	16 19	mpbird	⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
21	4	fneq1i	⊢ ( 𝐻 Fn ( 𝑅 × 𝑅 ) ↔ ( RingHom ↾ ( 𝑅 × 𝑅 ) ) Fn ( 𝑅 × 𝑅 ) )
22	20 21	sylibr	⊢ ( 𝜑 → 𝐻 Fn ( 𝑅 × 𝑅 ) )
23	5 7 12 22	rescval2	⊢ ( 𝜑 → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s 𝑅 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )