Step | Hyp | Ref
| Expression |
1 | | nllytop 21086 |
. . 3
⊢ (𝐽 ∈ 𝑛-Locally Comp
→ 𝐽 ∈
Top) |
2 | | resttop 20774 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ Top) |
3 | 1, 2 | sylan 487 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈
Top) |
4 | | elrest 15911 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴))) |
5 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝐽 ∈ 𝑛-Locally
Comp) |
6 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑢 ∈ 𝐽) |
7 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝑢 ∩ 𝐴) ⊆ 𝑢 |
8 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
9 | 7, 8 | sseldi 3566 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ 𝑢) |
10 | | nlly2i 21089 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
11 | 5, 6, 9, 10 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
12 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝐴) ∈ Top) |
13 | 1 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐽 ∈ Top) |
14 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ∈ (Clsd‘𝐽)) |
15 | | simprlr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ∈ 𝐽) |
16 | | elrestr 15912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
17 | 13, 14, 15, 16 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
18 | | simprr1 1102 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝑤) |
19 | | inss2 3796 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝐴) ⊆ 𝐴 |
20 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
21 | 19, 20 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝐴) |
22 | 18, 21 | elind 3760 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤 ∩ 𝐴)) |
23 | | opnneip 20733 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ (𝑤 ∩ 𝐴)) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
24 | 12, 17, 22, 23 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
25 | | simprr2 1103 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ⊆ 𝑠) |
26 | | ssrin 3800 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ⊆ 𝑠 → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) |
28 | | inss2 3796 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ⊆ 𝐴 |
29 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽 =
∪ 𝐽 |
30 | 29 | cldss 20643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐴 ⊆ ∪ 𝐽) |
31 | 14, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ⊆ ∪ 𝐽) |
32 | 29 | restuni 20776 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ 𝐴 = ∪ (𝐽
↾t 𝐴)) |
33 | 13, 31, 32 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
34 | 28, 33 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴)) |
35 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
36 | 35 | ssnei2 20730 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) ∧ ((𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴) ∧ (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
37 | 12, 24, 27, 34, 36 | syl22anc 1319 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
38 | | simprll 798 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢) |
39 | 38 | elpwid 4118 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ 𝑢) |
40 | | ssrin 3800 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ⊆ 𝑢 → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
42 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V |
43 | 42 | inex1 4727 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ∈ V |
44 | 43 | elpw 4114 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴) ↔ (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
45 | 41, 44 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴)) |
46 | 37, 45 | elind 3760 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
47 | 28 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝐴) |
48 | | restabs 20779 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝐴 ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
49 | 13, 47, 14, 48 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
50 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∩ 𝐴) ⊆ 𝑠 |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝑠) |
52 | | restabs 20779 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑢) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
53 | 13, 51, 38, 52 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
54 | 49, 53 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴))) |
55 | | simprr3 1104 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝑠) ∈ Comp) |
56 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) = (𝐴 ∩ 𝑠) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠) |
58 | | ineq1 3769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝐴 → (𝑣 ∩ 𝑠) = (𝐴 ∩ 𝑠)) |
59 | 58 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → ((𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠) ↔ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠))) |
60 | 59 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
61 | 14, 57, 60 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
62 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝐽) |
63 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ∪ 𝐽) |
65 | 39, 64 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝐽) |
66 | 29 | restcld 20786 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
67 | 13, 65, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
68 | 61, 67 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
69 | 56, 68 | syl5eqel 2692 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
70 | | cmpcld 21015 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑠) ∈ Comp ∧ (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
71 | 55, 69, 70 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
72 | 54, 71 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
73 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑠 ∩ 𝐴) → ((𝐽 ↾t 𝐴) ↾t 𝑣) = ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴))) |
74 | 73 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑠 ∩ 𝐴) → (((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp)) |
75 | 74 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴)) ∧ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
76 | 46, 72, 75 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
77 | 76 | expr 641 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽)) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
78 | 77 | rexlimdvva 3020 |
. . . . . . . . 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 678 |
. . . . . . 7
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝑢 ∩ 𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
81 | 80 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
82 | | pweq 4111 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∩ 𝐴) → 𝒫 𝑥 = 𝒫 (𝑢 ∩ 𝐴)) |
83 | 82 | ineq2d 3776 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
84 | 83 | rexeqdv 3122 |
. . . . . . 7
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
85 | 84 | raleqbi1dv 3123 |
. . . . . 6
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
86 | 81, 85 | syl5ibrcom 236 |
. . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
87 | 86 | rexlimdva 3013 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
88 | 4, 87 | sylbid 229 |
. . 3
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
89 | 88 | ralrimiv 2948 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
∀𝑥 ∈ (𝐽 ↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
90 | | isnlly 21082 |
. 2
⊢ ((𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp
↔ ((𝐽
↾t 𝐴)
∈ Top ∧ ∀𝑥
∈ (𝐽
↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
91 | 3, 89, 90 | sylanbrc 695 |
1
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈ 𝑛-Locally
Comp) |