Step | Hyp | Ref
| Expression |
1 | | rspecval 31320 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(Spec‘𝑅) =
((IDLsrg‘𝑅)
↾s (PrmIdeal‘𝑅))) |
2 | | rspecbas.1 |
. . . . 5
⊢ 𝑆 = (Spec‘𝑅) |
3 | | rspectopn.2 |
. . . . . 6
⊢ 𝑃 = (PrmIdeal‘𝑅) |
4 | 3 | oveq2i 7154 |
. . . . 5
⊢
((IDLsrg‘𝑅)
↾s 𝑃) =
((IDLsrg‘𝑅)
↾s (PrmIdeal‘𝑅)) |
5 | 1, 2, 4 | 3eqtr4g 2819 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑆 = ((IDLsrg‘𝑅) ↾s 𝑃)) |
6 | 5 | fveq2d 6655 |
. . 3
⊢ (𝑅 ∈ Ring →
(TopOpen‘𝑆) =
(TopOpen‘((IDLsrg‘𝑅) ↾s 𝑃))) |
7 | | eqid 2759 |
. . . 4
⊢
((IDLsrg‘𝑅)
↾s 𝑃) =
((IDLsrg‘𝑅)
↾s 𝑃) |
8 | | eqid 2759 |
. . . 4
⊢
(TopOpen‘(IDLsrg‘𝑅)) = (TopOpen‘(IDLsrg‘𝑅)) |
9 | 7, 8 | resstopn 21871 |
. . 3
⊢
((TopOpen‘(IDLsrg‘𝑅)) ↾t 𝑃) = (TopOpen‘((IDLsrg‘𝑅) ↾s 𝑃)) |
10 | 6, 9 | eqtr4di 2812 |
. 2
⊢ (𝑅 ∈ Ring →
(TopOpen‘𝑆) =
((TopOpen‘(IDLsrg‘𝑅)) ↾t 𝑃)) |
11 | | eqid 2759 |
. . . . 5
⊢
(IDLsrg‘𝑅) =
(IDLsrg‘𝑅) |
12 | | rspectopn.1 |
. . . . 5
⊢ 𝐼 = (LIdeal‘𝑅) |
13 | | eqid 2759 |
. . . . 5
⊢ ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) |
14 | 11, 12, 13 | idlsrgtset 31159 |
. . . 4
⊢ (𝑅 ∈ Ring → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (TopSet‘(IDLsrg‘𝑅))) |
15 | 12 | fvexi 6665 |
. . . . . . . . . . 11
⊢ 𝐼 ∈ V |
16 | 15 | rabex 5195 |
. . . . . . . . . 10
⊢ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) → {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ V) |
18 | | simp2 1135 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗) → 𝑗 ∈ 𝐼) |
19 | 11, 12 | idlsrgbas 31155 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝐼 =
(Base‘(IDLsrg‘𝑅))) |
20 | 19 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) → 𝐼 = (Base‘(IDLsrg‘𝑅))) |
21 | 20 | 3ad2ant1 1131 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗) → 𝐼 = (Base‘(IDLsrg‘𝑅))) |
22 | 18, 21 | eleqtrd 2853 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 𝐼 ∧ ¬ 𝑖 ⊆ 𝑗) → 𝑗 ∈ (Base‘(IDLsrg‘𝑅))) |
23 | 22 | rabssdv 3975 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) → {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ⊆ (Base‘(IDLsrg‘𝑅))) |
24 | 17, 23 | elpwd 4495 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐼) → {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ 𝒫
(Base‘(IDLsrg‘𝑅))) |
25 | 24 | ralrimiva 3111 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
∀𝑖 ∈ 𝐼 {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ 𝒫
(Base‘(IDLsrg‘𝑅))) |
26 | | eqid 2759 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) |
27 | 26 | rnmptss 6870 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐼 {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ 𝒫
(Base‘(IDLsrg‘𝑅)) → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⊆ 𝒫
(Base‘(IDLsrg‘𝑅))) |
28 | 25, 27 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⊆ 𝒫
(Base‘(IDLsrg‘𝑅))) |
29 | 14, 28 | eqsstrrd 3927 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(TopSet‘(IDLsrg‘𝑅)) ⊆ 𝒫
(Base‘(IDLsrg‘𝑅))) |
30 | | eqid 2759 |
. . . . . 6
⊢
(Base‘(IDLsrg‘𝑅)) = (Base‘(IDLsrg‘𝑅)) |
31 | | eqid 2759 |
. . . . . 6
⊢
(TopSet‘(IDLsrg‘𝑅)) = (TopSet‘(IDLsrg‘𝑅)) |
32 | 30, 31 | topnid 16752 |
. . . . 5
⊢
((TopSet‘(IDLsrg‘𝑅)) ⊆ 𝒫
(Base‘(IDLsrg‘𝑅)) → (TopSet‘(IDLsrg‘𝑅)) =
(TopOpen‘(IDLsrg‘𝑅))) |
33 | 29, 32 | syl 17 |
. . . 4
⊢ (𝑅 ∈ Ring →
(TopSet‘(IDLsrg‘𝑅)) = (TopOpen‘(IDLsrg‘𝑅))) |
34 | 14, 33 | eqtrd 2794 |
. . 3
⊢ (𝑅 ∈ Ring → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (TopOpen‘(IDLsrg‘𝑅))) |
35 | 34 | oveq1d 7158 |
. 2
⊢ (𝑅 ∈ Ring → (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) = ((TopOpen‘(IDLsrg‘𝑅)) ↾t 𝑃)) |
36 | 15 | mptex 6970 |
. . . . . . 7
⊢ (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V |
37 | 36 | rnex 7615 |
. . . . . 6
⊢ ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V |
38 | 3 | fvexi 6665 |
. . . . . 6
⊢ 𝑃 ∈ V |
39 | | elrest 16744 |
. . . . . 6
⊢ ((ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V ∧ 𝑃 ∈ V) → (𝑥 ∈ (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) ↔ ∃𝑦 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})𝑥 = (𝑦 ∩ 𝑃))) |
40 | 37, 38, 39 | mp2an 692 |
. . . . 5
⊢ (𝑥 ∈ (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) ↔ ∃𝑦 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})𝑥 = (𝑦 ∩ 𝑃)) |
41 | 16 | rgenw 3080 |
. . . . . . 7
⊢
∀𝑖 ∈
𝐼 {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ V |
42 | | ineq1 4105 |
. . . . . . . . 9
⊢ (𝑦 = {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} → (𝑦 ∩ 𝑃) = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃)) |
43 | 42 | eqeq2d 2770 |
. . . . . . . 8
⊢ (𝑦 = {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} → (𝑥 = (𝑦 ∩ 𝑃) ↔ 𝑥 = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃))) |
44 | 26, 43 | rexrnmptw 6845 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐼 {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ V → (∃𝑦 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})𝑥 = (𝑦 ∩ 𝑃) ↔ ∃𝑖 ∈ 𝐼 𝑥 = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃))) |
45 | 41, 44 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑦 ∈ ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})𝑥 = (𝑦 ∩ 𝑃) ↔ ∃𝑖 ∈ 𝐼 𝑥 = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃)) |
46 | | inrab2 4206 |
. . . . . . . . 9
⊢ ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃) = {𝑗 ∈ (𝐼 ∩ 𝑃) ∣ ¬ 𝑖 ⊆ 𝑗} |
47 | | prmidlssidl 31126 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(PrmIdeal‘𝑅) ⊆
(LIdeal‘𝑅)) |
48 | 47, 3, 12 | 3sstr4g 3933 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑃 ⊆ 𝐼) |
49 | | sseqin2 4116 |
. . . . . . . . . . 11
⊢ (𝑃 ⊆ 𝐼 ↔ (𝐼 ∩ 𝑃) = 𝑃) |
50 | 48, 49 | sylib 221 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → (𝐼 ∩ 𝑃) = 𝑃) |
51 | 50 | rabeqdv 3395 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → {𝑗 ∈ (𝐼 ∩ 𝑃) ∣ ¬ 𝑖 ⊆ 𝑗} = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
52 | 46, 51 | syl5eq 2806 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃) = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
53 | 52 | eqeq2d 2770 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑥 = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃) ↔ 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})) |
54 | 53 | rexbidv 3219 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∃𝑖 ∈ 𝐼 𝑥 = ({𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗} ∩ 𝑃) ↔ ∃𝑖 ∈ 𝐼 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})) |
55 | 45, 54 | syl5bb 286 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(∃𝑦 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})𝑥 = (𝑦 ∩ 𝑃) ↔ ∃𝑖 ∈ 𝐼 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})) |
56 | 40, 55 | syl5bb 286 |
. . . 4
⊢ (𝑅 ∈ Ring → (𝑥 ∈ (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) ↔ ∃𝑖 ∈ 𝐼 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})) |
57 | | rspectopn.3 |
. . . . . 6
⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
58 | 57 | eleq2i 2842 |
. . . . 5
⊢ (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})) |
59 | | eqid 2759 |
. . . . . 6
⊢ (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) = (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
60 | 38 | rabex 5195 |
. . . . . 6
⊢ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗} ∈ V |
61 | 59, 60 | elrnmpti 5794 |
. . . . 5
⊢ (𝑥 ∈ ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) ↔ ∃𝑖 ∈ 𝐼 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
62 | 58, 61 | bitri 278 |
. . . 4
⊢ (𝑥 ∈ 𝐽 ↔ ∃𝑖 ∈ 𝐼 𝑥 = {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) |
63 | 56, 62 | bitr4di 293 |
. . 3
⊢ (𝑅 ∈ Ring → (𝑥 ∈ (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) ↔ 𝑥 ∈ 𝐽)) |
64 | 63 | eqrdv 2757 |
. 2
⊢ (𝑅 ∈ Ring → (ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ↾t 𝑃) = 𝐽) |
65 | 10, 35, 64 | 3eqtr2rd 2801 |
1
⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆)) |