Metamath Proof Explorer


Theorem irinitoringc

Description: The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of Adamek p. 101 , and example in Lang p. 58. (Contributed by AV, 3-Apr-2020)

Ref Expression
Hypotheses irinitoringc.u φUV
irinitoringc.z φringU
irinitoringc.c C=RingCatU
Assertion irinitoringc φringInitOC

Proof

Step Hyp Ref Expression
1 irinitoringc.u φUV
2 irinitoringc.z φringU
3 irinitoringc.c C=RingCatU
4 zex V
5 4 mptex zzr1rV
6 eqid BaseC=BaseC
7 eqid HomC=HomC
8 3 6 1 7 ringchomfval φHomC=RingHomBaseC×BaseC
9 8 adantr φrBaseCHomC=RingHomBaseC×BaseC
10 9 oveqd φrBaseCringHomCr=ringRingHomBaseC×BaseCr
11 id ringUringU
12 zringring ringRing
13 12 a1i ringUringRing
14 11 13 elind ringUringURing
15 2 14 syl φringURing
16 3 6 1 ringcbas φBaseC=URing
17 15 16 eleqtrrd φringBaseC
18 17 adantr φrBaseCringBaseC
19 simpr φrBaseCrBaseC
20 18 19 ovresd φrBaseCringRingHomBaseC×BaseCr=ringRingHomr
21 16 eleq2d φrBaseCrURing
22 elin rURingrUrRing
23 22 simprbi rURingrRing
24 21 23 syl6bi φrBaseCrRing
25 24 imp φrBaseCrRing
26 eqid r=r
27 eqid zzr1r=zzr1r
28 eqid 1r=1r
29 26 27 28 mulgrhm2 rRingringRingHomr=zzr1r
30 25 29 syl φrBaseCringRingHomr=zzr1r
31 10 20 30 3eqtrd φrBaseCringHomCr=zzr1r
32 sneq f=zzr1rf=zzr1r
33 32 eqeq2d f=zzr1rringHomCr=fringHomCr=zzr1r
34 33 spcegv zzr1rVringHomCr=zzr1rfringHomCr=f
35 5 31 34 mpsyl φrBaseCfringHomCr=f
36 eusn ∃!ffringHomCrfringHomCr=f
37 35 36 sylibr φrBaseC∃!ffringHomCr
38 37 ralrimiva φrBaseC∃!ffringHomCr
39 3 ringccat UVCCat
40 1 39 syl φCCat
41 12 a1i φringRing
42 2 41 elind φringURing
43 42 16 eleqtrrd φringBaseC
44 6 7 40 43 isinito φringInitOCrBaseC∃!ffringHomCr
45 38 44 mpbird φringInitOC