This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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