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 | |
|
irinitoringc.z | |
||
irinitoringc.c | |
||
Assertion | irinitoringc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | irinitoringc.u | |
|
2 | irinitoringc.z | |
|
3 | irinitoringc.c | |
|
4 | zex | |
|
5 | 4 | mptex | |
6 | eqid | |
|
7 | eqid | |
|
8 | 3 6 1 7 | ringchomfval | |
9 | 8 | adantr | |
10 | 9 | oveqd | |
11 | id | |
|
12 | zringring | |
|
13 | 12 | a1i | |
14 | 11 13 | elind | |
15 | 2 14 | syl | |
16 | 3 6 1 | ringcbas | |
17 | 15 16 | eleqtrrd | |
18 | 17 | adantr | |
19 | simpr | |
|
20 | 18 19 | ovresd | |
21 | 16 | eleq2d | |
22 | elin | |
|
23 | 22 | simprbi | |
24 | 21 23 | syl6bi | |
25 | 24 | imp | |
26 | eqid | |
|
27 | eqid | |
|
28 | eqid | |
|
29 | 26 27 28 | mulgrhm2 | |
30 | 25 29 | syl | |
31 | 10 20 30 | 3eqtrd | |
32 | sneq | |
|
33 | 32 | eqeq2d | |
34 | 33 | spcegv | |
35 | 5 31 34 | mpsyl | |
36 | eusn | |
|
37 | 35 36 | sylibr | |
38 | 37 | ralrimiva | |
39 | 3 | ringccat | |
40 | 1 39 | syl | |
41 | 12 | a1i | |
42 | 2 41 | elind | |
43 | 42 16 | eleqtrrd | |
44 | 6 7 40 43 | isinito | |
45 | 38 44 | mpbird | |