Metamath Proof Explorer


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 ) , 𝐻 ⟩ ) )