Metamath Proof Explorer


Theorem dfringc2

Description: Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020)

Ref Expression
Hypotheses dfringc2.c 𝐶 = ( RingCat ‘ 𝑈 )
dfringc2.u ( 𝜑𝑈𝑉 )
dfringc2.b ( 𝜑𝐵 = ( 𝑈 ∩ Ring ) )
dfringc2.h ( 𝜑𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
dfringc2.o ( 𝜑· = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
Assertion dfringc2 ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )

Proof

Step Hyp Ref Expression
1 dfringc2.c 𝐶 = ( RingCat ‘ 𝑈 )
2 dfringc2.u ( 𝜑𝑈𝑉 )
3 dfringc2.b ( 𝜑𝐵 = ( 𝑈 ∩ Ring ) )
4 dfringc2.h ( 𝜑𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
5 dfringc2.o ( 𝜑· = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) )
6 1 2 3 4 ringcval ( 𝜑𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) )
7 eqid ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 )
8 fvexd ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) ∈ V )
9 inex1g ( 𝑈𝑉 → ( 𝑈 ∩ Ring ) ∈ V )
10 2 9 syl ( 𝜑 → ( 𝑈 ∩ Ring ) ∈ V )
11 3 10 eqeltrd ( 𝜑𝐵 ∈ V )
12 3 4 rhmresfn ( 𝜑𝐻 Fn ( 𝐵 × 𝐵 ) )
13 7 8 11 12 rescval2 ( 𝜑 → ( ( ExtStrCat ‘ 𝑈 ) ↾cat 𝐻 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
14 eqid ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
15 eqidd ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( 𝑥𝑈 , 𝑦𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
16 eqid ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( comp ‘ ( ExtStrCat ‘ 𝑈 ) )
17 14 2 16 estrccofval ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd𝑣 ) ) ↑m ( Base ‘ ( 1st𝑣 ) ) ) ↦ ( 𝑔𝑓 ) ) ) )
18 5 17 eqtrd ( 𝜑· = ( 𝑣 ∈ ( 𝑈 × 𝑈 ) , 𝑧𝑈 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ ( 2nd𝑣 ) ) ) , 𝑓 ∈ ( ( Base ‘ ( 2nd𝑣 ) ) ↑m ( Base ‘ ( 1st𝑣 ) ) ) ↦ ( 𝑔𝑓 ) ) ) )
19 14 2 15 18 estrcval ( 𝜑 → ( ExtStrCat ‘ 𝑈 ) = { ⟨ ( Base ‘ ndx ) , 𝑈 ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑥𝑈 , 𝑦𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
20 mpoexga ( ( 𝑈𝑉𝑈𝑉 ) → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∈ V )
21 2 2 20 syl2anc ( 𝜑 → ( 𝑥𝑈 , 𝑦𝑈 ↦ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∈ V )
22 fvexd ( 𝜑 → ( comp ‘ ( ExtStrCat ‘ 𝑈 ) ) ∈ V )
23 5 22 eqeltrd ( 𝜑· ∈ V )
24 rhmfn RingHom Fn ( Ring × Ring )
25 fnfun ( RingHom Fn ( Ring × Ring ) → Fun RingHom )
26 24 25 mp1i ( 𝜑 → Fun RingHom )
27 sqxpexg ( 𝐵 ∈ V → ( 𝐵 × 𝐵 ) ∈ V )
28 11 27 syl ( 𝜑 → ( 𝐵 × 𝐵 ) ∈ V )
29 resfunexg ( ( Fun RingHom ∧ ( 𝐵 × 𝐵 ) ∈ V ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
30 26 28 29 syl2anc ( 𝜑 → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
31 4 30 eqeltrd ( 𝜑𝐻 ∈ V )
32 inss1 ( 𝑈 ∩ Ring ) ⊆ 𝑈
33 3 32 eqsstrdi ( 𝜑𝐵𝑈 )
34 19 2 21 23 31 33 estrres ( 𝜑 → ( ( ( ExtStrCat ‘ 𝑈 ) ↾s 𝐵 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )
35 6 13 34 3eqtrd ( 𝜑𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } )