Step | Hyp | Ref
| Expression |
1 | | nllytop 21685 |
. . 3
⊢ (𝐽 ∈ 𝑛-Locally Comp
→ 𝐽 ∈
Top) |
2 | | resttop 21372 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ Top) |
3 | 1, 2 | sylan 575 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈
Top) |
4 | | elrest 16474 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴))) |
5 | | simpll 757 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝐽 ∈ 𝑛-Locally
Comp) |
6 | | simprl 761 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑢 ∈ 𝐽) |
7 | | inss1 4053 |
. . . . . . . . . . 11
⊢ (𝑢 ∩ 𝐴) ⊆ 𝑢 |
8 | | simprr 763 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
9 | 7, 8 | sseldi 3819 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ 𝑢) |
10 | | nlly2i 21688 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
11 | 5, 6, 9, 10 | syl3anc 1439 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) |
12 | 3 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝐴) ∈ Top) |
13 | 1 | ad3antrrr 720 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐽 ∈ Top) |
14 | | simpllr 766 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ∈ (Clsd‘𝐽)) |
15 | | simprlr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ∈ 𝐽) |
16 | | elrestr 16475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
17 | 13, 14, 15, 16 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
18 | | simprr1 1244 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝑤) |
19 | | inss2 4054 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝐴) ⊆ 𝐴 |
20 | | simplrr 768 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) |
21 | 19, 20 | sseldi 3819 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝐴) |
22 | 18, 21 | elind 4021 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤 ∩ 𝐴)) |
23 | | opnneip 21331 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ (𝑤 ∩ 𝐴)) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
24 | 12, 17, 22, 23 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
25 | | simprr2 1246 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ⊆ 𝑠) |
26 | 25 | ssrind 4060 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) |
27 | | inss2 4054 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ⊆ 𝐴 |
28 | | eqid 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽 =
∪ 𝐽 |
29 | 28 | cldss 21241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐴 ⊆ ∪ 𝐽) |
30 | 14, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ⊆ ∪ 𝐽) |
31 | 28 | restuni 21374 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ 𝐴 = ∪ (𝐽
↾t 𝐴)) |
32 | 13, 30, 31 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
33 | 27, 32 | syl5sseq 3872 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴)) |
34 | | eqid 2778 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
35 | 34 | ssnei2 21328 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) ∧ ((𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴) ∧ (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
36 | 12, 24, 26, 33, 35 | syl22anc 829 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) |
37 | | simprll 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢) |
38 | 37 | elpwid 4391 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ 𝑢) |
39 | 38 | ssrind 4060 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
40 | | vex 3401 |
. . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V |
41 | 40 | inex1 5036 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ∈ V |
42 | 41 | elpw 4385 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴) ↔ (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) |
43 | 39, 42 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴)) |
44 | 36, 43 | elind 4021 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
45 | 27 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝐴) |
46 | | restabs 21377 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝐴 ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
47 | 13, 45, 14, 46 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
48 | | inss1 4053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∩ 𝐴) ⊆ 𝑠 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝑠) |
50 | | restabs 21377 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑢) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
51 | 13, 49, 37, 50 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) |
52 | 47, 51 | eqtr4d 2817 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴))) |
53 | | simprr3 1248 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝑠) ∈ Comp) |
54 | | incom 4028 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) = (𝐴 ∩ 𝑠) |
55 | | eqid 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠) |
56 | | ineq1 4030 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → (𝑣 ∩ 𝑠) = (𝐴 ∩ 𝑠)) |
57 | 56 | rspceeqv 3529 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
58 | 14, 55, 57 | sylancl 580 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) |
59 | | simplrl 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝐽) |
60 | | elssuni 4702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ∪ 𝐽) |
62 | 38, 61 | sstrd 3831 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝐽) |
63 | 28 | restcld 21384 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
64 | 13, 62, 63 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) |
65 | 58, 64 | mpbird 249 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
66 | 54, 65 | syl5eqel 2863 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) |
67 | | cmpcld 21614 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑠) ∈ Comp ∧ (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
68 | 53, 66, 67 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
69 | 52, 68 | eqeltrd 2859 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) |
70 | | oveq2 6930 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑠 ∩ 𝐴) → ((𝐽 ↾t 𝐴) ↾t 𝑣) = ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴))) |
71 | 70 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑠 ∩ 𝐴) → (((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp)) |
72 | 71 | rspcev 3511 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴)) ∧ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
73 | 44, 69, 72 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
74 | 73 | expr 450 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽)) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
75 | 74 | rexlimdvva 3221 |
. . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → (∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
76 | 11, 75 | mpd 15 |
. . . . . . . 8
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
77 | 76 | anassrs 461 |
. . . . . . 7
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝑢 ∩ 𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
78 | 77 | ralrimiva 3148 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
79 | | pweq 4382 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∩ 𝐴) → 𝒫 𝑥 = 𝒫 (𝑢 ∩ 𝐴)) |
80 | 79 | ineq2d 4037 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) |
81 | 80 | rexeqdv 3341 |
. . . . . . 7
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
82 | 81 | raleqbi1dv 3328 |
. . . . . 6
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
83 | 78, 82 | syl5ibrcom 239 |
. . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
84 | 83 | rexlimdva 3213 |
. . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
85 | 4, 84 | sylbid 232 |
. . 3
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
86 | 85 | ralrimiv 3147 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
∀𝑥 ∈ (𝐽 ↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) |
87 | | isnlly 21681 |
. 2
⊢ ((𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp
↔ ((𝐽
↾t 𝐴)
∈ Top ∧ ∀𝑥
∈ (𝐽
↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) |
88 | 3, 86, 87 | sylanbrc 578 |
1
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈ 𝑛-Locally
Comp) |