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