# Metamath Proof Explorer

## Theorem nzerooringczr

Description: There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in Adamek p. 103. (Contributed by AV, 18-Apr-2020)

Ref Expression
Hypotheses nzerooringczr.u ${⊢}{\phi }\to {U}\in {V}$
nzerooringczr.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
nzerooringczr.z ${⊢}{\phi }\to {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$
nzerooringczr.e ${⊢}{\phi }\to {Z}\in {U}$
nzerooringczr.i ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {U}$
Assertion nzerooringczr ${⊢}{\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 nzerooringczr.u ${⊢}{\phi }\to {U}\in {V}$
2 nzerooringczr.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
3 nzerooringczr.z ${⊢}{\phi }\to {Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)$
4 nzerooringczr.e ${⊢}{\phi }\to {Z}\in {U}$
5 nzerooringczr.i ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {U}$
6 ax-1 ${⊢}\mathrm{ZeroO}\left({C}\right)=\varnothing \to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
7 neq0 ${⊢}¬\mathrm{ZeroO}\left({C}\right)=\varnothing ↔\exists {h}\phantom{\rule{.4em}{0ex}}{h}\in \mathrm{ZeroO}\left({C}\right)$
8 2 ringccat ${⊢}{U}\in {V}\to {C}\in \mathrm{Cat}$
9 1 8 syl ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
10 iszeroi ${⊢}\left({C}\in \mathrm{Cat}\wedge {h}\in \mathrm{ZeroO}\left({C}\right)\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)$
11 9 10 sylan ${⊢}\left({\phi }\wedge {h}\in \mathrm{ZeroO}\left({C}\right)\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)$
12 1 2 3 4 zrtermoringc ${⊢}{\phi }\to {Z}\in \mathrm{TermO}\left({C}\right)$
13 1 5 2 irinitoringc ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)$
14 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to {C}\in \mathrm{Cat}$
15 simplr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to {h}\in \mathrm{InitO}\left({C}\right)$
16 simpr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)$
17 14 15 16 initoeu1w ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to {h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}$
18 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to {C}\in \mathrm{Cat}$
19 simpr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to {Z}\in \mathrm{TermO}\left({C}\right)$
20 simplr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to {h}\in \mathrm{TermO}\left({C}\right)$
21 18 19 20 termoeu1w ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to {Z}{\simeq }_{𝑐}\left({C}\right){h}$
22 cictr ${⊢}\left({C}\in \mathrm{Cat}\wedge {Z}{\simeq }_{𝑐}\left({C}\right){h}\wedge {h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\to {Z}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}$
23 9 22 syl3an1 ${⊢}\left({\phi }\wedge {Z}{\simeq }_{𝑐}\left({C}\right){h}\wedge {h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\to {Z}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}$
24 eqid ${⊢}\mathrm{Iso}\left({C}\right)=\mathrm{Iso}\left({C}\right)$
25 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
26 3 eldifad ${⊢}{\phi }\to {Z}\in \mathrm{Ring}$
27 4 26 elind ${⊢}{\phi }\to {Z}\in \left({U}\cap \mathrm{Ring}\right)$
28 2 25 1 ringcbas ${⊢}{\phi }\to {\mathrm{Base}}_{{C}}={U}\cap \mathrm{Ring}$
29 27 28 eleqtrrd ${⊢}{\phi }\to {Z}\in {\mathrm{Base}}_{{C}}$
30 zringring ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
31 30 a1i ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \mathrm{Ring}$
32 5 31 elind ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in \left({U}\cap \mathrm{Ring}\right)$
33 32 28 eleqtrrd ${⊢}{\phi }\to {ℤ}_{\mathrm{ring}}\in {\mathrm{Base}}_{{C}}$
34 24 25 9 29 33 cic ${⊢}{\phi }\to \left({Z}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\right)$
35 n0 ${⊢}{Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\right)$
36 eqid ${⊢}\mathrm{Hom}\left({C}\right)=\mathrm{Hom}\left({C}\right)$
37 25 36 24 9 29 33 isohom ${⊢}{\phi }\to {Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\subseteq {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}$
38 ssn0 ${⊢}\left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\subseteq {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\wedge {Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \right)\to {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing$
39 2 25 1 36 29 33 ringchom ${⊢}{\phi }\to {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}={Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}$
40 39 neeq1d ${⊢}{\phi }\to \left({Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing ↔{Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}\ne \varnothing \right)$
41 zringnzr ${⊢}{ℤ}_{\mathrm{ring}}\in \mathrm{NzRing}$
42 nrhmzr ${⊢}\left({Z}\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{NzRing}\right)\to {Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}=\varnothing$
43 3 41 42 sylancl ${⊢}{\phi }\to {Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}=\varnothing$
44 eqneqall ${⊢}{Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}=\varnothing \to \left({Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}\ne \varnothing \to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
45 43 44 syl ${⊢}{\phi }\to \left({Z}\mathrm{RingHom}{ℤ}_{\mathrm{ring}}\ne \varnothing \to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
46 40 45 sylbid ${⊢}{\phi }\to \left({Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
47 38 46 syl5com ${⊢}\left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\subseteq {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\wedge {Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \right)\to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
48 47 expcom ${⊢}{Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \to \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\subseteq {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)$
49 48 com13 ${⊢}{\phi }\to \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\subseteq {Z}\mathrm{Hom}\left({C}\right){ℤ}_{\mathrm{ring}}\to \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)$
50 37 49 mpd ${⊢}{\phi }\to \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\ne \varnothing \to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
51 35 50 syl5bir ${⊢}{\phi }\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({Z}\mathrm{Iso}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
52 34 51 sylbid ${⊢}{\phi }\to \left({Z}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
53 52 3ad2ant1 ${⊢}\left({\phi }\wedge {Z}{\simeq }_{𝑐}\left({C}\right){h}\wedge {h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\to \left({Z}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
54 23 53 mpd ${⊢}\left({\phi }\wedge {Z}{\simeq }_{𝑐}\left({C}\right){h}\wedge {h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing$
55 54 3exp ${⊢}{\phi }\to \left({Z}{\simeq }_{𝑐}\left({C}\right){h}\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)$
56 55 a1dd ${⊢}{\phi }\to \left({Z}{\simeq }_{𝑐}\left({C}\right){h}\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)$
57 56 ad2antrr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to \left({Z}{\simeq }_{𝑐}\left({C}\right){h}\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)$
58 21 57 mpd ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\wedge {Z}\in \mathrm{TermO}\left({C}\right)\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)$
59 58 exp31 ${⊢}{\phi }\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
60 59 com34 ${⊢}{\phi }\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
61 60 com25 ${⊢}{\phi }\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
62 61 ad2antrr ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to \left({h}{\simeq }_{𝑐}\left({C}\right){ℤ}_{\mathrm{ring}}\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
63 17 62 mpd ${⊢}\left(\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\wedge {ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)$
64 63 ex ${⊢}\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
65 64 com25 ${⊢}\left({\phi }\wedge {h}\in \mathrm{InitO}\left({C}\right)\right)\to \left({h}\in \mathrm{TermO}\left({C}\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
66 65 expimpd ${⊢}{\phi }\to \left(\left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
67 66 com23 ${⊢}{\phi }\to \left({h}\in {\mathrm{Base}}_{{C}}\to \left(\left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)\right)$
68 67 impd ${⊢}{\phi }\to \left(\left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)$
69 68 com24 ${⊢}{\phi }\to \left({ℤ}_{\mathrm{ring}}\in \mathrm{InitO}\left({C}\right)\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left(\left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)\right)$
70 13 69 mpd ${⊢}{\phi }\to \left({Z}\in \mathrm{TermO}\left({C}\right)\to \left(\left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)\right)$
71 12 70 mpd ${⊢}{\phi }\to \left(\left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
72 71 adantr ${⊢}\left({\phi }\wedge {h}\in \mathrm{ZeroO}\left({C}\right)\right)\to \left(\left({h}\in {\mathrm{Base}}_{{C}}\wedge \left({h}\in \mathrm{InitO}\left({C}\right)\wedge {h}\in \mathrm{TermO}\left({C}\right)\right)\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
73 11 72 mpd ${⊢}\left({\phi }\wedge {h}\in \mathrm{ZeroO}\left({C}\right)\right)\to \mathrm{ZeroO}\left({C}\right)=\varnothing$
74 73 expcom ${⊢}{h}\in \mathrm{ZeroO}\left({C}\right)\to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
75 74 exlimiv ${⊢}\exists {h}\phantom{\rule{.4em}{0ex}}{h}\in \mathrm{ZeroO}\left({C}\right)\to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
76 7 75 sylbi ${⊢}¬\mathrm{ZeroO}\left({C}\right)=\varnothing \to \left({\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing \right)$
77 6 76 pm2.61i ${⊢}{\phi }\to \mathrm{ZeroO}\left({C}\right)=\varnothing$