| Step | Hyp | Ref
| Expression |
| 1 | | zartop.1 |
. . . 4
⊢ 𝑆 = (Spec‘𝑅) |
| 2 | | zartop.2 |
. . . 4
⊢ 𝐽 = (TopOpen‘𝑆) |
| 3 | 1, 2 | zartop 33875 |
. . 3
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top) |
| 4 | | sseq2 4010 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑥 → (𝑥 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑥)) |
| 5 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) → 𝑥 ∈ (PrmIdeal‘𝑅)) |
| 6 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) → 𝑥 ⊆ 𝑥) |
| 7 | 4, 5, 6 | elrabd 3694 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) → 𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) |
| 9 | | sseq1 4009 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑖 ⊆ 𝑗)) |
| 10 | 9 | rabbidv 3444 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 11 | 10 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗}) = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 12 | | crngring 20242 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑅 ∈ Ring) |
| 14 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑥 ∈ (PrmIdeal‘𝑅)) |
| 15 | | prmidlidl 33472 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) → 𝑥 ∈ (LIdeal‘𝑅)) |
| 16 | 13, 14, 15 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑥 ∈ (LIdeal‘𝑅)) |
| 17 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(PrmIdeal‘𝑅)
∈ V |
| 18 | 17 | rabex 5339 |
. . . . . . . . . . . . 13
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ∈ V |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ∈ V) |
| 20 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑥 → (𝑖 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑗)) |
| 21 | 20 | rabbidv 3444 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑥 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) |
| 22 | 21 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑥 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑖 = 𝑥) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 24 | 11, 16, 19, 23 | elrnmptdv 5976 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})) |
| 25 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) → 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) |
| 26 | 25 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) → (𝑥 ∈ 𝑑 ↔ 𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗})) |
| 27 | 25 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) → (𝑦 ∈ 𝑑 ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗})) |
| 28 | 26, 27 | bibi12d 345 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) → ((𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) ↔ (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}))) |
| 29 | 24, 28 | rspcdv 3614 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → (∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}))) |
| 30 | 29 | imp 406 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗})) |
| 31 | 8, 30 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗}) |
| 32 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑦 → (𝑥 ⊆ 𝑗 ↔ 𝑥 ⊆ 𝑦)) |
| 33 | 32 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} ↔ (𝑦 ∈ (PrmIdeal‘𝑅) ∧ 𝑥 ⊆ 𝑦)) |
| 34 | 33 | simprbi 496 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑥 ⊆ 𝑗} → 𝑥 ⊆ 𝑦) |
| 35 | 31, 34 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑥 ⊆ 𝑦) |
| 36 | | sseq2 4010 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑦 → (𝑦 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑦)) |
| 37 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ∈ (PrmIdeal‘𝑅)) |
| 38 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ⊆ 𝑦) |
| 39 | 36, 37, 38 | elrabd 3694 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) |
| 40 | 39 | ad4ant13 751 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) |
| 41 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ∈ (PrmIdeal‘𝑅)) |
| 42 | | prmidlidl 33472 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ∈ (LIdeal‘𝑅)) |
| 43 | 13, 41, 42 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → 𝑦 ∈ (LIdeal‘𝑅)) |
| 44 | 17 | rabex 5339 |
. . . . . . . . . . . . 13
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ∈ V |
| 45 | 44 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ∈ V) |
| 46 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑦 → (𝑖 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑗)) |
| 47 | 46 | rabbidv 3444 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑦 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) |
| 48 | 47 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑦 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑖 = 𝑦) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
| 50 | 11, 43, 45, 49 | elrnmptdv 5976 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})) |
| 51 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) → 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) |
| 52 | 51 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) → (𝑥 ∈ 𝑑 ↔ 𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗})) |
| 53 | 51 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) → (𝑦 ∈ 𝑑 ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗})) |
| 54 | 52, 53 | bibi12d 345 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ 𝑑 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) → ((𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) ↔ (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}))) |
| 55 | 50, 54 | rspcdv 3614 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → (∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}))) |
| 56 | 55 | imp 406 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ↔ 𝑦 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗})) |
| 57 | 40, 56 | mpbird 257 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗}) |
| 58 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑥 → (𝑦 ⊆ 𝑗 ↔ 𝑦 ⊆ 𝑥)) |
| 59 | 58 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} ↔ (𝑥 ∈ (PrmIdeal‘𝑅) ∧ 𝑦 ⊆ 𝑥)) |
| 60 | 59 | simprbi 496 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑦 ⊆ 𝑗} → 𝑦 ⊆ 𝑥) |
| 61 | 57, 60 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑦 ⊆ 𝑥) |
| 62 | 35, 61 | eqssd 4001 |
. . . . . 6
⊢ ((((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) ∧ ∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑)) → 𝑥 = 𝑦) |
| 63 | 62 | ex 412 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑥 ∈ (PrmIdeal‘𝑅)) ∧ 𝑦 ∈ (PrmIdeal‘𝑅)) → (∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)) |
| 64 | 63 | anasss 466 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑥 ∈ (PrmIdeal‘𝑅) ∧ 𝑦 ∈ (PrmIdeal‘𝑅))) → (∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)) |
| 65 | 64 | ralrimivva 3202 |
. . 3
⊢ (𝑅 ∈ CRing →
∀𝑥 ∈
(PrmIdeal‘𝑅)∀𝑦 ∈ (PrmIdeal‘𝑅)(∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)) |
| 66 | 3, 65 | jca 511 |
. 2
⊢ (𝑅 ∈ CRing → (𝐽 ∈ Top ∧ ∀𝑥 ∈ (PrmIdeal‘𝑅)∀𝑦 ∈ (PrmIdeal‘𝑅)(∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦))) |
| 67 | | eqid 2737 |
. . . . 5
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
| 68 | 1, 2, 67 | zartopon 33876 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅))) |
| 69 | | toponuni 22920 |
. . . 4
⊢ (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) → (PrmIdeal‘𝑅) = ∪ 𝐽) |
| 70 | 68, 69 | syl 17 |
. . 3
⊢ (𝑅 ∈ CRing →
(PrmIdeal‘𝑅) = ∪ 𝐽) |
| 71 | 1, 2, 67, 11 | zartopn 33874 |
. . . 4
⊢ (𝑅 ∈ CRing → (𝐽 ∈
(TopOn‘(PrmIdeal‘𝑅)) ∧ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗}) = (Clsd‘𝐽))) |
| 72 | 71 | simprd 495 |
. . 3
⊢ (𝑅 ∈ CRing → ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗}) = (Clsd‘𝐽)) |
| 73 | 70, 72 | ist0cld 33832 |
. 2
⊢ (𝑅 ∈ CRing → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ (PrmIdeal‘𝑅)∀𝑦 ∈ (PrmIdeal‘𝑅)(∀𝑑 ∈ ran (𝑘 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑘 ⊆ 𝑗})(𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)))) |
| 74 | 66, 73 | mpbird 257 |
1
⊢ (𝑅 ∈ CRing → 𝐽 ∈ Kol2) |