Proof of Theorem elcls
| Step | Hyp | Ref
| Expression |
| 1 | | clscld.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
| 2 | 1 | cmclsopn 23070 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) |
| 3 | 2 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽) |
| 5 | | eldif 3961 |
. . . . . . 7
⊢ (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ↔ (𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
| 6 | 5 | biimpri 228 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑋 ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) |
| 7 | 6 | 3ad2antl3 1188 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → 𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) |
| 8 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
| 9 | 1 | sscls 23064 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
| 10 | 8, 9 | ssind 4241 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑋 ∩ ((cls‘𝐽)‘𝑆))) |
| 11 | | dfin4 4278 |
. . . . . . . . . 10
⊢ (𝑋 ∩ ((cls‘𝐽)‘𝑆)) = (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) |
| 12 | 10, 11 | sseqtrdi 4024 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))) |
| 13 | | reldisj 4453 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → ((𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅ ↔ 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆))))) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅ ↔ 𝑆 ⊆ (𝑋 ∖ (𝑋 ∖ ((cls‘𝐽)‘𝑆))))) |
| 15 | 12, 14 | mpbird 257 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅) |
| 16 | | nne 2944 |
. . . . . . . . 9
⊢ (¬
((𝑋 ∖
((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = ∅) |
| 17 | | incom 4209 |
. . . . . . . . . 10
⊢ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) |
| 18 | 17 | eqeq1i 2742 |
. . . . . . . . 9
⊢ (((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) = ∅ ↔ (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅) |
| 19 | 16, 18 | bitri 275 |
. . . . . . . 8
⊢ (¬
((𝑋 ∖
((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅ ↔ (𝑆 ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑆))) = ∅) |
| 20 | 15, 19 | sylibr 234 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅) |
| 21 | 20 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅) |
| 23 | | eleq2 2830 |
. . . . . . 7
⊢ (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (𝑃 ∈ 𝑥 ↔ 𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)))) |
| 24 | | ineq1 4213 |
. . . . . . . . 9
⊢ (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (𝑥 ∩ 𝑆) = ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆)) |
| 25 | 24 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → ((𝑥 ∩ 𝑆) ≠ ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)) |
| 26 | 25 | notbid 318 |
. . . . . . 7
⊢ (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → (¬ (𝑥 ∩ 𝑆) ≠ ∅ ↔ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)) |
| 27 | 23, 26 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑆)) → ((𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅) ↔ (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∧ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅))) |
| 28 | 27 | rspcev 3622 |
. . . . 5
⊢ (((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽 ∧ (𝑃 ∈ (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∧ ¬ ((𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∩ 𝑆) ≠ ∅)) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅)) |
| 29 | 4, 7, 22, 28 | syl12anc 837 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅)) |
| 30 | | incom 4209 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∩ 𝑥) = (𝑥 ∩ 𝑆) |
| 31 | 30 | eqeq1i 2742 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∩ 𝑥) = ∅ ↔ (𝑥 ∩ 𝑆) = ∅) |
| 32 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ 𝑆) ≠ ∅ ↔ ¬ (𝑥 ∩ 𝑆) = ∅) |
| 33 | 32 | con2bii 357 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∩ 𝑆) = ∅ ↔ ¬ (𝑥 ∩ 𝑆) ≠ ∅) |
| 34 | 31, 33 | bitri 275 |
. . . . . . . . . . 11
⊢ ((𝑆 ∩ 𝑥) = ∅ ↔ ¬ (𝑥 ∩ 𝑆) ≠ ∅) |
| 35 | 1 | opncld 23041 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽) → (𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
| 36 | 35 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽)) |
| 37 | | reldisj 4453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ 𝑋 → ((𝑆 ∩ 𝑥) = ∅ ↔ 𝑆 ⊆ (𝑋 ∖ 𝑥))) |
| 38 | 37 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ⊆ 𝑋 ∧ (𝑆 ∩ 𝑥) = ∅) → 𝑆 ⊆ (𝑋 ∖ 𝑥)) |
| 39 | 38 | ad4ant24 754 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ (𝑆 ∩ 𝑥) = ∅) → 𝑆 ⊆ (𝑋 ∖ 𝑥)) |
| 40 | 1 | clsss2 23080 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∖ 𝑥) ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ (𝑋 ∖ 𝑥)) → ((cls‘𝐽)‘𝑆) ⊆ (𝑋 ∖ 𝑥)) |
| 41 | 36, 39, 40 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ (𝑆 ∩ 𝑥) = ∅) → ((cls‘𝐽)‘𝑆) ⊆ (𝑋 ∖ 𝑥)) |
| 42 | 41 | sseld 3982 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ (𝑆 ∩ 𝑥) = ∅) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → 𝑃 ∈ (𝑋 ∖ 𝑥))) |
| 43 | | eldifn 4132 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ (𝑋 ∖ 𝑥) → ¬ 𝑃 ∈ 𝑥) |
| 44 | 42, 43 | syl6 35 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ (𝑆 ∩ 𝑥) = ∅) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) → ¬ 𝑃 ∈ 𝑥)) |
| 45 | 44 | con2d 134 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ (𝑆 ∩ 𝑥) = ∅) → (𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
| 46 | 34, 45 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅) → (𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
| 47 | 46 | exp31 419 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑥 ∈ 𝐽 → (¬ (𝑥 ∩ 𝑆) ≠ ∅ → (𝑃 ∈ 𝑥 → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))))) |
| 48 | 47 | com34 91 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑥 ∈ 𝐽 → (𝑃 ∈ 𝑥 → (¬ (𝑥 ∩ 𝑆) ≠ ∅ → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))))) |
| 49 | 48 | imp4a 422 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑥 ∈ 𝐽 → ((𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)))) |
| 50 | 49 | rexlimdv 3153 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆))) |
| 51 | 50 | imp 406 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) |
| 52 | 51 | 3adantl3 1169 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅)) → ¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) |
| 53 | 29, 52 | impbida 801 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅))) |
| 54 | | rexanali 3102 |
. . 3
⊢
(∃𝑥 ∈
𝐽 (𝑃 ∈ 𝑥 ∧ ¬ (𝑥 ∩ 𝑆) ≠ ∅) ↔ ¬ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)) |
| 55 | 53, 54 | bitrdi 287 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (¬ 𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ¬ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |
| 56 | 55 | con4bid 317 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))) |