Proof of Theorem iscnrm3llem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sseq2 4009 | . . 3
⊢ (𝑙 = (𝑛 ∩ 𝑍) → (𝐶 ⊆ 𝑙 ↔ 𝐶 ⊆ (𝑛 ∩ 𝑍))) | 
| 2 |  | ineq1 4212 | . . . 4
⊢ (𝑙 = (𝑛 ∩ 𝑍) → (𝑙 ∩ 𝑘) = ((𝑛 ∩ 𝑍) ∩ 𝑘)) | 
| 3 | 2 | eqeq1d 2738 | . . 3
⊢ (𝑙 = (𝑛 ∩ 𝑍) → ((𝑙 ∩ 𝑘) = ∅ ↔ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅)) | 
| 4 | 1, 3 | 3anbi13d 1439 | . 2
⊢ (𝑙 = (𝑛 ∩ 𝑍) → ((𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅) ↔ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ 𝑘 ∧ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅))) | 
| 5 |  | sseq2 4009 | . . 3
⊢ (𝑘 = (𝑚 ∩ 𝑍) → (𝐷 ⊆ 𝑘 ↔ 𝐷 ⊆ (𝑚 ∩ 𝑍))) | 
| 6 |  | ineq2 4213 | . . . 4
⊢ (𝑘 = (𝑚 ∩ 𝑍) → ((𝑛 ∩ 𝑍) ∩ 𝑘) = ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍))) | 
| 7 | 6 | eqeq1d 2738 | . . 3
⊢ (𝑘 = (𝑚 ∩ 𝑍) → (((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅ ↔ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅)) | 
| 8 | 5, 7 | 3anbi23d 1440 | . 2
⊢ (𝑘 = (𝑚 ∩ 𝑍) → ((𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ 𝑘 ∧ ((𝑛 ∩ 𝑍) ∩ 𝑘) = ∅) ↔ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅))) | 
| 9 |  | simp11 1203 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐽 ∈ Top) | 
| 10 |  | simp121 1305 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑍 ∈ 𝒫 ∪ 𝐽) | 
| 11 |  | simp2l 1199 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑛 ∈ 𝐽) | 
| 12 |  | elrestr 17474 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝑛 ∈ 𝐽) → (𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) | 
| 13 | 9, 10, 11, 12 | syl3anc 1372 | . . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) | 
| 14 |  | simp2r 1200 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑚 ∈ 𝐽) | 
| 15 |  | elrestr 17474 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝑚 ∈ 𝐽) → (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) | 
| 16 | 9, 10, 14, 15 | syl3anc 1372 | . . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍)) | 
| 17 |  | simp31 1209 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ 𝑛) | 
| 18 |  | eqidd 2737 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ∪ 𝐽 =
∪ 𝐽) | 
| 19 | 10 | elpwid 4608 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝑍 ⊆ ∪ 𝐽) | 
| 20 |  | eqidd 2737 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝐽 ↾t 𝑍) = (𝐽 ↾t 𝑍)) | 
| 21 |  | simp122 1306 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ∈ (Clsd‘(𝐽 ↾t 𝑍))) | 
| 22 | 9, 18, 19, 20, 21 | restcls2lem 48817 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ 𝑍) | 
| 23 | 17, 22 | ssind 4240 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐶 ⊆ (𝑛 ∩ 𝑍)) | 
| 24 |  | simp32 1210 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ 𝑚) | 
| 25 |  | simp123 1307 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ∈ (Clsd‘(𝐽 ↾t 𝑍))) | 
| 26 | 9, 18, 19, 20, 25 | restcls2lem 48817 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ 𝑍) | 
| 27 | 24, 26 | ssind 4240 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → 𝐷 ⊆ (𝑚 ∩ 𝑍)) | 
| 28 |  | inss1 4236 | . . . . . . 7
⊢ (𝑛 ∩ 𝑍) ⊆ 𝑛 | 
| 29 |  | inss1 4236 | . . . . . . 7
⊢ (𝑚 ∩ 𝑍) ⊆ 𝑚 | 
| 30 |  | ss2in 4244 | . . . . . . 7
⊢ (((𝑛 ∩ 𝑍) ⊆ 𝑛 ∧ (𝑚 ∩ 𝑍) ⊆ 𝑚) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ (𝑛 ∩ 𝑚)) | 
| 31 | 28, 29, 30 | mp2an 692 | . . . . . 6
⊢ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ (𝑛 ∩ 𝑚) | 
| 32 |  | simp33 1211 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝑛 ∩ 𝑚) = ∅) | 
| 33 | 31, 32 | sseqtrid 4025 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ ∅) | 
| 34 |  | ss0 4401 | . . . . 5
⊢ (((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) ⊆ ∅ → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅) | 
| 35 | 33, 34 | syl 17 | . . . 4
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅) | 
| 36 | 23, 27, 35 | 3jca 1128 | . . 3
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅)) | 
| 37 | 13, 16, 36 | 3jca 1128 | . 2
⊢ (((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) ∧ (𝑛 ∈ 𝐽 ∧ 𝑚 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)) → ((𝑛 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍) ∧ (𝑚 ∩ 𝑍) ∈ (𝐽 ↾t 𝑍) ∧ (𝐶 ⊆ (𝑛 ∩ 𝑍) ∧ 𝐷 ⊆ (𝑚 ∩ 𝑍) ∧ ((𝑛 ∩ 𝑍) ∩ (𝑚 ∩ 𝑍)) = ∅))) | 
| 38 | 4, 8, 37 | iscnrm3lem7 48843 | 1
⊢ ((𝐽 ∈ Top ∧ (𝑍 ∈ 𝒫 ∪ 𝐽
∧ 𝐶 ∈
(Clsd‘(𝐽
↾t 𝑍))
∧ 𝐷 ∈
(Clsd‘(𝐽
↾t 𝑍)))
∧ (𝐶 ∩ 𝐷) = ∅) →
(∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝐶 ⊆ 𝑛 ∧ 𝐷 ⊆ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅) → ∃𝑙 ∈ (𝐽 ↾t 𝑍)∃𝑘 ∈ (𝐽 ↾t 𝑍)(𝐶 ⊆ 𝑙 ∧ 𝐷 ⊆ 𝑘 ∧ (𝑙 ∩ 𝑘) = ∅))) |