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 ⊢ φ → U ∈ V
nzerooringczr.c ⊢ C = RingCat ⁡ U
nzerooringczr.z ⊢ φ → Z ∈ Ring ∖ NzRing
nzerooringczr.e ⊢ φ → Z ∈ U
nzerooringczr.i ⊢ φ → ℤ ring ∈ U
Assertion nzerooringczr ⊢ φ → ZeroO ⁡ C = ∅

Proof

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