Step | Hyp | Ref
| Expression |
1 | | nllytop 21276 |
. . 3
⊢ (𝐽 ∈ 𝑛-Locally Comp
→ 𝐽 ∈
Top) |
2 | | resttop 20964 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ Top) |
3 | 1, 2 | sylan 488 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈
Top) |
4 | | elrest 16088 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴))) |
5 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝐽 ∈ 𝑛-Locally
Comp) |
6 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑢 ∈ 𝐽) |
7 | | inss1 3833 |
. . . . . . . . . . 11
⊢ (𝑢 ∩ 𝐴) ⊆ 𝑢 |
8 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
9 | 7, 8 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ 𝑢) |
10 | | nlly2i 21279 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
11 | 5, 6, 9, 10 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
12 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝐴) ∈ Top) |
13 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐽 ∈ Top) |
14 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ∈ (Clsd‘𝐽)) |
15 | | simprlr 803 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ∈ 𝐽) |
16 | | elrestr 16089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
17 | 13, 14, 15, 16 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
18 | | simprr1 1109 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝑤) |
19 | | inss2 3834 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝐴) ⊆ 𝐴 |
20 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
21 | 19, 20 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝐴) |
22 | 18, 21 | elind 3798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤 ∩ 𝐴)) |
23 | | opnneip 20923 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ (𝑤 ∩ 𝐴)) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
24 | 12, 17, 22, 23 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
25 | | simprr2 1110 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ⊆ 𝑠) |
26 | | ssrin 3838 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ⊆ 𝑠 → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) |
28 | | inss2 3834 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ⊆ 𝐴 |
29 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽 =
∪ 𝐽 |
30 | 29 | cldss 20833 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐴 ⊆ ∪ 𝐽) |
31 | 14, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ⊆ ∪ 𝐽) |
32 | 29 | restuni 20966 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ 𝐴 = ∪ (𝐽
↾t 𝐴)) |
33 | 13, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
34 | 28, 33 | syl5sseq 3653 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴)) |
35 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
36 | 35 | ssnei2 20920 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) ∧ ((𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴) ∧ (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
37 | 12, 24, 27, 34, 36 | syl22anc 1327 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
38 | | simprll 802 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢) |
39 | 38 | elpwid 4170 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ 𝑢) |
40 | | ssrin 3838 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ 𝑢 → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
42 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V |
43 | 42 | inex1 4799 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ∈ V |
44 | 43 | elpw 4164 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴) ↔ (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
45 | 41, 44 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴)) |
46 | 37, 45 | elind 3798 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
47 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝐴) |
48 | | restabs 20969 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝐴 ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
49 | 13, 47, 14, 48 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
50 | | inss1 3833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∩ 𝐴) ⊆ 𝑠 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝑠) |
52 | | restabs 20969 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑢) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
53 | 13, 51, 38, 52 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
54 | 49, 53 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴))) |
55 | | simprr3 1111 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝑠) ∈ Comp) |
56 | | incom 3805 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) = (𝐴 ∩ 𝑠) |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠) |
58 | | ineq1 3807 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐴 → (𝑣 ∩ 𝑠) = (𝐴 ∩ 𝑠)) |
59 | 58 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → ((𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠) ↔ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠))) |
60 | 59 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
61 | 14, 57, 60 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
62 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝐽) |
63 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ∪ 𝐽) |
65 | 39, 64 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝐽) |
66 | 29 | restcld 20976 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
67 | 13, 65, 66 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
68 | 61, 67 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
69 | 56, 68 | syl5eqel 2705 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
70 | | cmpcld 21205 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑠) ∈ Comp ∧ (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
71 | 55, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
72 | 54, 71 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
73 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑠 ∩ 𝐴) → ((𝐽 ↾t 𝐴) ↾t 𝑣) = ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴))) |
74 | 73 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑠 ∩ 𝐴) → (((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp)) |
75 | 74 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴)) ∧ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
76 | 46, 72, 75 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
77 | 76 | expr 643 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽)) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
78 | 77 | rexlimdvva 3038 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → (∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
79 | 11, 78 | mpd 15 |
. . . . . . . 8
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
80 | 79 | anassrs 680 |
. . . . . . 7
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝑢 ∩ 𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
81 | 80 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
82 | | pweq 4161 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∩ 𝐴) → 𝒫 𝑥 = 𝒫 (𝑢 ∩ 𝐴)) |
83 | 82 | ineq2d 3814 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
84 | 83 | rexeqdv 3145 |
. . . . . . 7
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
85 | 84 | raleqbi1dv 3146 |
. . . . . 6
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
86 | 81, 85 | syl5ibrcom 237 |
. . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
87 | 86 | rexlimdva 3031 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
88 | 4, 87 | sylbid 230 |
. . 3
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
89 | 88 | ralrimiv 2965 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
∀𝑥 ∈ (𝐽 ↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
90 | | isnlly 21272 |
. 2
⊢ ((𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp
↔ ((𝐽
↾t 𝐴)
∈ Top ∧ ∀𝑥
∈ (𝐽
↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
91 | 3, 89, 90 | sylanbrc 698 |
1
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈ 𝑛-Locally
Comp) |