Proof of Theorem iscnrm3llem2
Step | Hyp | Ref
| Expression |
1 | | sseq2 3932 |
. . 3
⊢ (𝑙 = (𝑛 ∩ 𝑍) → (𝐶 ⊆ 𝑙 ↔ 𝐶 ⊆ (𝑛 ∩ 𝑍))) |
2 | | ineq1 4125 |
. . . 4
⊢ (𝑙 = (𝑛 ∩ 𝑍) → (𝑙 ∩ 𝑘) = ((𝑛 ∩ 𝑍) ∩ 𝑘)) |
3 | 2 | eqeq1d 2739 |
. . 3
⊢ (𝑙 = (𝑛 ∩ 𝑍) → ((𝑙 ∩ 𝑘) = ∅ ↔ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅)) |
4 | 1, 3 | 3anbi13d 1440 |
. 2
⊢ (𝑙 = (𝑛 ∩ 𝑍) → ((𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅) ↔ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ 𝑘 ∧ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅))) |
5 | | sseq2 3932 |
. . 3
⊢ (𝑘 = (𝑚 ∩ 𝑍) → (𝐷 ⊆ 𝑘 ↔ 𝐷 ⊆ (𝑚 ∩ 𝑍))) |
6 | | ineq2 4126 |
. . . 4
⊢ (𝑘 = (𝑚 ∩ 𝑍) → ((𝑛 ∩ 𝑍) ∩ 𝑘) = ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍))) |
7 | 6 | eqeq1d 2739 |
. . 3
⊢ (𝑘 = (𝑚 ∩ 𝑍) → (((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅ ↔ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅)) |
8 | 5, 7 | 3anbi23d 1441 |
. 2
⊢ (𝑘 = (𝑚 ∩ 𝑍) → ((𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ 𝑘 ∧ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅) ↔ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅))) |
9 | | simp11 1205 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐽 ∈ Top) |
10 | | simp121 1307 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑍 ∈ 𝒫 ∪ 𝐽) |
11 | | simp2l 1201 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑛 ∈ 𝐽) |
12 | | elrestr 16938 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝑛 ∈ 𝐽) → (𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) |
13 | 9, 10, 11, 12 | syl3anc 1373 |
. . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) |
14 | | simp2r 1202 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑚 ∈ 𝐽) |
15 | | elrestr 16938 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝑚 ∈ 𝐽) → (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) |
16 | 9, 10, 14, 15 | syl3anc 1373 |
. . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) |
17 | | simp31 1211 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ 𝑛) |
18 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ∪ 𝐽 =
∪ 𝐽) |
19 | 10 | elpwid 4529 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑍 ⊆ ∪ 𝐽) |
20 | | eqidd 2738 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝐽 ↾t 𝑍) = (𝐽 ↾t 𝑍)) |
21 | | simp122 1308 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍))) |
22 | 9, 18, 19, 20, 21 | restcls2lem 45887 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ 𝑍) |
23 | 17, 22 | ssind 4152 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ (𝑛 ∩ 𝑍)) |
24 | | simp32 1212 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ 𝑚) |
25 | | simp123 1309 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) |
26 | 9, 18, 19, 20, 25 | restcls2lem 45887 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ 𝑍) |
27 | 24, 26 | ssind 4152 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ (𝑚 ∩ 𝑍)) |
28 | | inss1 4148 |
. . . . . . 7
⊢ (𝑛 ∩ 𝑍) ⊆ 𝑛 |
29 | | inss1 4148 |
. . . . . . 7
⊢ (𝑚 ∩ 𝑍) ⊆ 𝑚 |
30 | | ss2in 4156 |
. . . . . . 7
⊢ (((𝑛 ∩ 𝑍) ⊆ 𝑛 ∧ (𝑚 ∩ 𝑍) ⊆ 𝑚) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ (𝑛 ∩ 𝑚)) |
31 | 28, 29, 30 | mp2an 692 |
. . . . . 6
⊢ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ (𝑛 ∩ 𝑚) |
32 | | simp33 1213 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑛 ∩ 𝑚) = ∅) |
33 | 31, 32 | sseqtrid 3958 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ ∅) |
34 | | ss0 4318 |
. . . . 5
⊢ (((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ ∅ → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅) |
35 | 33, 34 | syl 17 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅) |
36 | 23, 27, 35 | 3jca 1130 |
. . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅)) |
37 | 13, 16, 36 | 3jca 1130 |
. 2
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍) ∧ (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍) ∧ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅))) |
38 | 4, 8, 37 | iscnrm3lem7 45914 |
1
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) →
(∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅))) |