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 bitrid 
 |-  ( 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 ) )