| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . 5
⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋) |
| 2 | | restcld.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
| 3 | 2 | topopn 22912 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
| 4 | | ssexg 5323 |
. . . . 5
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V) |
| 5 | 1, 3, 4 | syl2anr 597 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) |
| 6 | | resttop 23168 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top) |
| 7 | 5, 6 | syldan 591 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top) |
| 8 | | eqid 2737 |
. . . 4
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
| 9 | 8 | iscld 23035 |
. . 3
⊢ ((𝐽 ↾t 𝑆) ∈ Top → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
| 10 | 7, 9 | syl 17 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
| 11 | 2 | restuni 23170 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
| 12 | 11 | sseq2d 4016 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ⊆ 𝑆 ↔ 𝐴 ⊆ ∪ (𝐽 ↾t 𝑆))) |
| 13 | 11 | difeq1d 4125 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝐴) = (∪ (𝐽 ↾t 𝑆) ∖ 𝐴)) |
| 14 | 13 | eleq1d 2826 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (∪
(𝐽 ↾t
𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))) |
| 15 | 12, 14 | anbi12d 632 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
| 16 | | elrest 17472 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆))) |
| 17 | 5, 16 | syldan 591 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆))) |
| 18 | 17 | anbi2d 630 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)))) |
| 19 | 2 | opncld 23041 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽)) |
| 20 | 19 | ad5ant14 758 |
. . . . . . 7
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽)) |
| 21 | | incom 4209 |
. . . . . . . . . . . 12
⊢ (𝑋 ∩ 𝑆) = (𝑆 ∩ 𝑋) |
| 22 | | dfss2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝑋 ↔ (𝑆 ∩ 𝑋) = 𝑆) |
| 23 | 22 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∩ 𝑋) = 𝑆) |
| 24 | 21, 23 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝑋 → (𝑋 ∩ 𝑆) = 𝑆) |
| 25 | 24 | ad4antlr 733 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∩ 𝑆) = 𝑆) |
| 26 | 25 | difeq1d 4125 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ((𝑋 ∩ 𝑆) ∖ 𝑜) = (𝑆 ∖ 𝑜)) |
| 27 | | difeq2 4120 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ (𝑜 ∩ 𝑆))) |
| 28 | | difindi 4292 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆)) |
| 29 | | difid 4376 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∖ 𝑆) = ∅ |
| 30 | 29 | uneq2i 4165 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ ∅) |
| 31 | | un0 4394 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ 𝑜) ∪ ∅) = (𝑆 ∖ 𝑜) |
| 32 | 28, 30, 31 | 3eqtri 2769 |
. . . . . . . . . . 11
⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = (𝑆 ∖ 𝑜) |
| 33 | 27, 32 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜)) |
| 34 | 33 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜)) |
| 35 | | dfss4 4269 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝑆 ↔ (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
| 36 | 35 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝑆 → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
| 37 | 36 | ad3antlr 731 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
| 38 | 26, 34, 37 | 3eqtr2rd 2784 |
. . . . . . . 8
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∩ 𝑆) ∖ 𝑜)) |
| 39 | 21 | difeq1i 4122 |
. . . . . . . . 9
⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑆 ∩ 𝑋) ∖ 𝑜) |
| 40 | | indif2 4281 |
. . . . . . . . 9
⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑆 ∩ 𝑋) ∖ 𝑜) |
| 41 | | incom 4209 |
. . . . . . . . 9
⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑋 ∖ 𝑜) ∩ 𝑆) |
| 42 | 39, 40, 41 | 3eqtr2i 2771 |
. . . . . . . 8
⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑋 ∖ 𝑜) ∩ 𝑆) |
| 43 | 38, 42 | eqtrdi 2793 |
. . . . . . 7
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆)) |
| 44 | | ineq1 4213 |
. . . . . . . 8
⊢ (𝑥 = (𝑋 ∖ 𝑜) → (𝑥 ∩ 𝑆) = ((𝑋 ∖ 𝑜) ∩ 𝑆)) |
| 45 | 44 | rspceeqv 3645 |
. . . . . . 7
⊢ (((𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)) |
| 46 | 20, 43, 45 | syl2anc 584 |
. . . . . 6
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)) |
| 47 | 46 | rexlimdva2 3157 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) → (∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
| 48 | 47 | expimpd 453 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
| 49 | 18, 48 | sylbid 240 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
| 50 | | difindi 4292 |
. . . . . . . . . 10
⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆)) |
| 51 | 29 | uneq2i 4165 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ ∅) |
| 52 | | un0 4394 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝑥) ∪ ∅) = (𝑆 ∖ 𝑥) |
| 53 | 50, 51, 52 | 3eqtri 2769 |
. . . . . . . . 9
⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = (𝑆 ∖ 𝑥) |
| 54 | | difin2 4301 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
| 56 | 53, 55 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
| 57 | 56 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
| 58 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top) |
| 59 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑆 ∈ V) |
| 60 | 2 | cldopn 23039 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑥) ∈ 𝐽) |
| 61 | 60 | adantl 481 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑥) ∈ 𝐽) |
| 62 | | elrestr 17473 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V ∧ (𝑋 ∖ 𝑥) ∈ 𝐽) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
| 63 | 58, 59, 61, 62 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
| 64 | 57, 63 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)) |
| 65 | | inss2 4238 |
. . . . . 6
⊢ (𝑥 ∩ 𝑆) ⊆ 𝑆 |
| 66 | 64, 65 | jctil 519 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))) |
| 67 | | sseq1 4009 |
. . . . . 6
⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ↔ (𝑥 ∩ 𝑆) ⊆ 𝑆)) |
| 68 | | difeq2 4120 |
. . . . . . 7
⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝑆 ∖ 𝐴) = (𝑆 ∖ (𝑥 ∩ 𝑆))) |
| 69 | 68 | eleq1d 2826 |
. . . . . 6
⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))) |
| 70 | 67, 69 | anbi12d 632 |
. . . . 5
⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)))) |
| 71 | 66, 70 | syl5ibrcom 247 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
| 72 | 71 | rexlimdva 3155 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
| 73 | 49, 72 | impbid 212 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
| 74 | 10, 15, 73 | 3bitr2d 307 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |