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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
nzerooringczr.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
nzerooringczr.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
nzerooringczr.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
nzerooringczr.i ⊢ ( 𝜑 → ℤring ∈ 𝑈 )
Assertion nzerooringczr ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ∅ )

Proof

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