Metamath Proof Explorer


Theorem zrninitoringc

Description: The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020)

Ref Expression
Hypotheses zrtermoringc.u
|- ( ph -> U e. V )
zrtermoringc.c
|- C = ( RingCat ` U )
zrtermoringc.z
|- ( ph -> Z e. ( Ring \ NzRing ) )
zrtermoringc.e
|- ( ph -> Z e. U )
zrninitoringc.e
|- ( ph -> E. r e. ( Base ` C ) r e. NzRing )
Assertion zrninitoringc
|- ( ph -> Z e/ ( InitO ` C ) )

Proof

Step Hyp Ref Expression
1 zrtermoringc.u
 |-  ( ph -> U e. V )
2 zrtermoringc.c
 |-  C = ( RingCat ` U )
3 zrtermoringc.z
 |-  ( ph -> Z e. ( Ring \ NzRing ) )
4 zrtermoringc.e
 |-  ( ph -> Z e. U )
5 zrninitoringc.e
 |-  ( ph -> E. r e. ( Base ` C ) r e. NzRing )
6 eqid
 |-  ( Base ` C ) = ( Base ` C )
7 1 ad2antrr
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> U e. V )
8 eqid
 |-  ( Hom ` C ) = ( Hom ` C )
9 3 eldifad
 |-  ( ph -> Z e. Ring )
10 4 9 elind
 |-  ( ph -> Z e. ( U i^i Ring ) )
11 2 6 1 ringcbas
 |-  ( ph -> ( Base ` C ) = ( U i^i Ring ) )
12 10 11 eleqtrrd
 |-  ( ph -> Z e. ( Base ` C ) )
13 12 ad2antrr
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> Z e. ( Base ` C ) )
14 simplr
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> r e. ( Base ` C ) )
15 2 6 7 8 13 14 ringchom
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> ( Z ( Hom ` C ) r ) = ( Z RingHom r ) )
16 3 adantr
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> Z e. ( Ring \ NzRing ) )
17 nrhmzr
 |-  ( ( Z e. ( Ring \ NzRing ) /\ r e. NzRing ) -> ( Z RingHom r ) = (/) )
18 16 17 sylan
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> ( Z RingHom r ) = (/) )
19 15 18 eqtrd
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> ( Z ( Hom ` C ) r ) = (/) )
20 eq0
 |-  ( ( Z ( Hom ` C ) r ) = (/) <-> A. h -. h e. ( Z ( Hom ` C ) r ) )
21 19 20 sylib
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> A. h -. h e. ( Z ( Hom ` C ) r ) )
22 alnex
 |-  ( A. h -. h e. ( Z ( Hom ` C ) r ) <-> -. E. h h e. ( Z ( Hom ` C ) r ) )
23 21 22 sylib
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> -. E. h h e. ( Z ( Hom ` C ) r ) )
24 euex
 |-  ( E! h h e. ( Z ( Hom ` C ) r ) -> E. h h e. ( Z ( Hom ` C ) r ) )
25 23 24 nsyl
 |-  ( ( ( ph /\ r e. ( Base ` C ) ) /\ r e. NzRing ) -> -. E! h h e. ( Z ( Hom ` C ) r ) )
26 25 ex
 |-  ( ( ph /\ r e. ( Base ` C ) ) -> ( r e. NzRing -> -. E! h h e. ( Z ( Hom ` C ) r ) ) )
27 26 reximdva
 |-  ( ph -> ( E. r e. ( Base ` C ) r e. NzRing -> E. r e. ( Base ` C ) -. E! h h e. ( Z ( Hom ` C ) r ) ) )
28 5 27 mpd
 |-  ( ph -> E. r e. ( Base ` C ) -. E! h h e. ( Z ( Hom ` C ) r ) )
29 rexnal
 |-  ( E. r e. ( Base ` C ) -. E! h h e. ( Z ( Hom ` C ) r ) <-> -. A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) )
30 28 29 sylib
 |-  ( ph -> -. A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) )
31 df-nel
 |-  ( Z e/ ( InitO ` C ) <-> -. Z e. ( InitO ` C ) )
32 2 ringccat
 |-  ( U e. V -> C e. Cat )
33 1 32 syl
 |-  ( ph -> C e. Cat )
34 6 8 33 12 isinito
 |-  ( ph -> ( Z e. ( InitO ` C ) <-> A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) ) )
35 34 notbid
 |-  ( ph -> ( -. Z e. ( InitO ` C ) <-> -. A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) ) )
36 31 35 syl5bb
 |-  ( ph -> ( Z e/ ( InitO ` C ) <-> -. A. r e. ( Base ` C ) E! h h e. ( Z ( Hom ` C ) r ) ) )
37 30 36 mpbird
 |-  ( ph -> Z e/ ( InitO ` C ) )