Step | Hyp | Ref
| Expression |
1 | | zrninitoringc.e |
. . . 4
β’ (π β βπ β (BaseβπΆ)π β NzRing) |
2 | | zrtermoringc.c |
. . . . . . . . . . 11
β’ πΆ = (RingCatβπ) |
3 | | eqid 2737 |
. . . . . . . . . . 11
β’
(BaseβπΆ) =
(BaseβπΆ) |
4 | | zrtermoringc.u |
. . . . . . . . . . . 12
β’ (π β π β π) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β π β π) |
6 | | eqid 2737 |
. . . . . . . . . . 11
β’ (Hom
βπΆ) = (Hom
βπΆ) |
7 | | zrtermoringc.e |
. . . . . . . . . . . . . 14
β’ (π β π β π) |
8 | | zrtermoringc.z |
. . . . . . . . . . . . . . 15
β’ (π β π β (Ring β
NzRing)) |
9 | 8 | eldifad 3927 |
. . . . . . . . . . . . . 14
β’ (π β π β Ring) |
10 | 7, 9 | elind 4159 |
. . . . . . . . . . . . 13
β’ (π β π β (π β© Ring)) |
11 | 2, 3, 4 | ringcbas 46383 |
. . . . . . . . . . . . 13
β’ (π β (BaseβπΆ) = (π β© Ring)) |
12 | 10, 11 | eleqtrrd 2841 |
. . . . . . . . . . . 12
β’ (π β π β (BaseβπΆ)) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β π β (BaseβπΆ)) |
14 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β π β (BaseβπΆ)) |
15 | 2, 3, 5, 6, 13, 14 | ringchom 46385 |
. . . . . . . . . 10
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β (π(Hom βπΆ)π) = (π RingHom π)) |
16 | 8 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (BaseβπΆ)) β π β (Ring β
NzRing)) |
17 | | nrhmzr 46245 |
. . . . . . . . . . 11
β’ ((π β (Ring β NzRing)
β§ π β NzRing)
β (π RingHom π) = β
) |
18 | 16, 17 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β (π RingHom π) = β
) |
19 | 15, 18 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β (π(Hom βπΆ)π) = β
) |
20 | | eq0 4308 |
. . . . . . . . 9
β’ ((π(Hom βπΆ)π) = β
β ββ Β¬ β β (π(Hom βπΆ)π)) |
21 | 19, 20 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β ββ Β¬ β β (π(Hom βπΆ)π)) |
22 | | alnex 1784 |
. . . . . . . 8
β’
(ββ Β¬
β β (π(Hom βπΆ)π) β Β¬ ββ β β (π(Hom βπΆ)π)) |
23 | 21, 22 | sylib 217 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β Β¬ ββ β β (π(Hom βπΆ)π)) |
24 | | euex 2576 |
. . . . . . 7
β’
(β!β β β (π(Hom βπΆ)π) β ββ β β (π(Hom βπΆ)π)) |
25 | 23, 24 | nsyl 140 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ π β NzRing) β Β¬ β!β β β (π(Hom βπΆ)π)) |
26 | 25 | ex 414 |
. . . . 5
β’ ((π β§ π β (BaseβπΆ)) β (π β NzRing β Β¬ β!β β β (π(Hom βπΆ)π))) |
27 | 26 | reximdva 3166 |
. . . 4
β’ (π β (βπ β (BaseβπΆ)π β NzRing β βπ β (BaseβπΆ) Β¬ β!β β β (π(Hom βπΆ)π))) |
28 | 1, 27 | mpd 15 |
. . 3
β’ (π β βπ β (BaseβπΆ) Β¬ β!β β β (π(Hom βπΆ)π)) |
29 | | rexnal 3104 |
. . 3
β’
(βπ β
(BaseβπΆ) Β¬
β!β β β (π(Hom βπΆ)π) β Β¬ βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π)) |
30 | 28, 29 | sylib 217 |
. 2
β’ (π β Β¬ βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π)) |
31 | | df-nel 3051 |
. . 3
β’ (π β (InitOβπΆ) β Β¬ π β (InitOβπΆ)) |
32 | 2 | ringccat 46396 |
. . . . . 6
β’ (π β π β πΆ β Cat) |
33 | 4, 32 | syl 17 |
. . . . 5
β’ (π β πΆ β Cat) |
34 | 3, 6, 33, 12 | isinito 17889 |
. . . 4
β’ (π β (π β (InitOβπΆ) β βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π))) |
35 | 34 | notbid 318 |
. . 3
β’ (π β (Β¬ π β (InitOβπΆ) β Β¬ βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π))) |
36 | 31, 35 | bitrid 283 |
. 2
β’ (π β (π β (InitOβπΆ) β Β¬ βπ β (BaseβπΆ)β!β β β (π(Hom βπΆ)π))) |
37 | 30, 36 | mpbird 257 |
1
β’ (π β π β (InitOβπΆ)) |