Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋) |
2 | | restcld.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
3 | 2 | topopn 22036 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
4 | | ssexg 5250 |
. . . . 5
⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V) |
5 | 1, 3, 4 | syl2anr 596 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V) |
6 | | resttop 22292 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top) |
7 | 5, 6 | syldan 590 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top) |
8 | | eqid 2739 |
. . . 4
⊢ ∪ (𝐽
↾t 𝑆) =
∪ (𝐽 ↾t 𝑆) |
9 | 8 | iscld 22159 |
. . 3
⊢ ((𝐽 ↾t 𝑆) ∈ Top → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
10 | 7, 9 | syl 17 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
11 | 2 | restuni 22294 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆)) |
12 | 11 | sseq2d 3957 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ⊆ 𝑆 ↔ 𝐴 ⊆ ∪ (𝐽 ↾t 𝑆))) |
13 | 11 | difeq1d 4060 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝐴) = (∪ (𝐽 ↾t 𝑆) ∖ 𝐴)) |
14 | 13 | eleq1d 2824 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (∪
(𝐽 ↾t
𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))) |
15 | 12, 14 | anbi12d 630 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽
↾t 𝑆)
∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
16 | | elrest 17119 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆))) |
17 | 5, 16 | syldan 590 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆))) |
18 | 17 | anbi2d 628 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)))) |
19 | 2 | opncld 22165 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽)) |
20 | 19 | ad5ant14 754 |
. . . . . . 7
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽)) |
21 | | incom 4139 |
. . . . . . . . . . . 12
⊢ (𝑋 ∩ 𝑆) = (𝑆 ∩ 𝑋) |
22 | | df-ss 3908 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ 𝑋 ↔ (𝑆 ∩ 𝑋) = 𝑆) |
23 | 22 | biimpi 215 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∩ 𝑋) = 𝑆) |
24 | 21, 23 | eqtrid 2791 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ 𝑋 → (𝑋 ∩ 𝑆) = 𝑆) |
25 | 24 | ad4antlr 729 |
. . . . . . . . . 10
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∩ 𝑆) = 𝑆) |
26 | 25 | difeq1d 4060 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ((𝑋 ∩ 𝑆) ∖ 𝑜) = (𝑆 ∖ 𝑜)) |
27 | | difeq2 4055 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ (𝑜 ∩ 𝑆))) |
28 | | difindi 4220 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆)) |
29 | | difid 4309 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∖ 𝑆) = ∅ |
30 | 29 | uneq2i 4098 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ ∅) |
31 | | un0 4329 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ 𝑜) ∪ ∅) = (𝑆 ∖ 𝑜) |
32 | 28, 30, 31 | 3eqtri 2771 |
. . . . . . . . . . 11
⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = (𝑆 ∖ 𝑜) |
33 | 27, 32 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜)) |
34 | 33 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜)) |
35 | | dfss4 4197 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝑆 ↔ (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
36 | 35 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝑆 → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
37 | 36 | ad3antlr 727 |
. . . . . . . . 9
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴) |
38 | 26, 34, 37 | 3eqtr2rd 2786 |
. . . . . . . 8
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∩ 𝑆) ∖ 𝑜)) |
39 | 21 | difeq1i 4057 |
. . . . . . . . 9
⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑆 ∩ 𝑋) ∖ 𝑜) |
40 | | indif2 4209 |
. . . . . . . . 9
⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑆 ∩ 𝑋) ∖ 𝑜) |
41 | | incom 4139 |
. . . . . . . . 9
⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑋 ∖ 𝑜) ∩ 𝑆) |
42 | 39, 40, 41 | 3eqtr2i 2773 |
. . . . . . . 8
⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑋 ∖ 𝑜) ∩ 𝑆) |
43 | 38, 42 | eqtrdi 2795 |
. . . . . . 7
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆)) |
44 | | ineq1 4144 |
. . . . . . . 8
⊢ (𝑥 = (𝑋 ∖ 𝑜) → (𝑥 ∩ 𝑆) = ((𝑋 ∖ 𝑜) ∩ 𝑆)) |
45 | 44 | rspceeqv 3575 |
. . . . . . 7
⊢ (((𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)) |
46 | 20, 43, 45 | syl2anc 583 |
. . . . . 6
⊢
(((((𝐽 ∈ Top
∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)) |
47 | 46 | rexlimdva2 3217 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) → (∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
48 | 47 | expimpd 453 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
49 | 18, 48 | sylbid 239 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
50 | | difindi 4220 |
. . . . . . . . . 10
⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆)) |
51 | 29 | uneq2i 4098 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ ∅) |
52 | | un0 4329 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ 𝑥) ∪ ∅) = (𝑆 ∖ 𝑥) |
53 | 50, 51, 52 | 3eqtri 2771 |
. . . . . . . . 9
⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = (𝑆 ∖ 𝑥) |
54 | | difin2 4230 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
56 | 53, 55 | eqtrid 2791 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆)) |
58 | | simpll 763 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top) |
59 | 5 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑆 ∈ V) |
60 | 2 | cldopn 22163 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑥) ∈ 𝐽) |
61 | 60 | adantl 481 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑥) ∈ 𝐽) |
62 | | elrestr 17120 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V ∧ (𝑋 ∖ 𝑥) ∈ 𝐽) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
63 | 58, 59, 61, 62 | syl3anc 1369 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆)) |
64 | 57, 63 | eqeltrd 2840 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)) |
65 | | inss2 4168 |
. . . . . 6
⊢ (𝑥 ∩ 𝑆) ⊆ 𝑆 |
66 | 64, 65 | jctil 519 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))) |
67 | | sseq1 3950 |
. . . . . 6
⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ↔ (𝑥 ∩ 𝑆) ⊆ 𝑆)) |
68 | | difeq2 4055 |
. . . . . . 7
⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝑆 ∖ 𝐴) = (𝑆 ∖ (𝑥 ∩ 𝑆))) |
69 | 68 | eleq1d 2824 |
. . . . . 6
⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))) |
70 | 67, 69 | anbi12d 630 |
. . . . 5
⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)))) |
71 | 66, 70 | syl5ibrcom 246 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
72 | 71 | rexlimdva 3214 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))) |
73 | 49, 72 | impbid 211 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |
74 | 10, 15, 73 | 3bitr2d 306 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) |