| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nllytop 23482 | . . 3
⊢ (𝐽 ∈ 𝑛-Locally Comp
→ 𝐽 ∈
Top) | 
| 2 |  | resttop 23169 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ Top) | 
| 3 | 1, 2 | sylan 580 | . 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈
Top) | 
| 4 |  | elrest 17473 | . . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴))) | 
| 5 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝐽 ∈ 𝑛-Locally
Comp) | 
| 6 |  | simprl 770 | . . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑢 ∈ 𝐽) | 
| 7 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) | 
| 8 | 7 | elin1d 4203 | . . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → 𝑦 ∈ 𝑢) | 
| 9 |  | nlly2i 23485 | . . . . . . . . . 10
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝑢 ∈ 𝐽 ∧ 𝑦 ∈ 𝑢) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) | 
| 10 | 5, 6, 8, 9 | syl3anc 1372 | . . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp)) | 
| 11 | 3 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝐴) ∈ Top) | 
| 12 | 1 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐽 ∈ Top) | 
| 13 |  | simpllr 775 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ∈ (Clsd‘𝐽)) | 
| 14 |  | simprlr 779 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ∈ 𝐽) | 
| 15 |  | elrestr 17474 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) | 
| 16 | 12, 13, 14, 15 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) | 
| 17 |  | simprr1 1221 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝑤) | 
| 18 |  | simplrr 777 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢 ∩ 𝐴)) | 
| 19 | 18 | elin2d 4204 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ 𝐴) | 
| 20 | 17, 19 | elind 4199 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤 ∩ 𝐴)) | 
| 21 |  | opnneip 23128 | . . . . . . . . . . . . . . 15
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ (𝑤 ∩ 𝐴)) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) | 
| 22 | 11, 16, 20, 21 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) | 
| 23 |  | simprr2 1222 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑤 ⊆ 𝑠) | 
| 24 | 23 | ssrind 4243 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴)) | 
| 25 |  | inss2 4237 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ⊆ 𝐴 | 
| 26 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 27 | 26 | cldss 23038 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐴 ⊆ ∪ 𝐽) | 
| 28 | 13, 27 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 ⊆ ∪ 𝐽) | 
| 29 | 26 | restuni 23171 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽)
→ 𝐴 = ∪ (𝐽
↾t 𝐴)) | 
| 30 | 12, 28, 29 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | 
| 31 | 25, 30 | sseqtrid 4025 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴)) | 
| 32 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) | 
| 33 | 32 | ssnei2 23125 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ↾t 𝐴) ∈ Top ∧ (𝑤 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) ∧ ((𝑤 ∩ 𝐴) ⊆ (𝑠 ∩ 𝐴) ∧ (𝑠 ∩ 𝐴) ⊆ ∪
(𝐽 ↾t
𝐴))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) | 
| 34 | 11, 22, 24, 31, 33 | syl22anc 838 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})) | 
| 35 |  | simprll 778 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢) | 
| 36 | 35 | elpwid 4608 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ 𝑢) | 
| 37 | 36 | ssrind 4243 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) | 
| 38 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑠 ∈ V | 
| 39 | 38 | inex1 5316 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) ∈ V | 
| 40 | 39 | elpw 4603 | . . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴) ↔ (𝑠 ∩ 𝐴) ⊆ (𝑢 ∩ 𝐴)) | 
| 41 | 37, 40 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ 𝒫 (𝑢 ∩ 𝐴)) | 
| 42 | 34, 41 | elind 4199 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) | 
| 43 | 25 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝐴) | 
| 44 |  | restabs 23174 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝐴 ∧ 𝐴 ∈ (Clsd‘𝐽)) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) | 
| 45 | 12, 43, 13, 44 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) | 
| 46 |  | inss1 4236 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∩ 𝐴) ⊆ 𝑠 | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ⊆ 𝑠) | 
| 48 |  | restabs 23174 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ (𝑠 ∩ 𝐴) ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑢) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) | 
| 49 | 12, 47, 35, 48 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) = (𝐽 ↾t (𝑠 ∩ 𝐴))) | 
| 50 | 45, 49 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) = ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴))) | 
| 51 |  | simprr3 1223 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐽 ↾t 𝑠) ∈ Comp) | 
| 52 |  | incom 4208 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∩ 𝐴) = (𝐴 ∩ 𝑠) | 
| 53 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠) | 
| 54 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝐴 → (𝑣 ∩ 𝑠) = (𝐴 ∩ 𝑠)) | 
| 55 | 54 | rspceeqv 3644 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴 ∩ 𝑠) = (𝐴 ∩ 𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) | 
| 56 | 13, 53, 55 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠)) | 
| 57 |  | simplrl 776 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝐽) | 
| 58 |  | elssuni 4936 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝐽 → 𝑢 ⊆ ∪ 𝐽) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑢 ⊆ ∪ 𝐽) | 
| 60 | 36, 59 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝐽) | 
| 61 | 26 | restcld 23181 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑠 ⊆ ∪ 𝐽)
→ ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) | 
| 62 | 12, 60, 61 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴 ∩ 𝑠) = (𝑣 ∩ 𝑠))) | 
| 63 | 56, 62 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝐴 ∩ 𝑠) ∈ (Clsd‘(𝐽 ↾t 𝑠))) | 
| 64 | 52, 63 | eqeltrid 2844 | . . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) | 
| 65 |  | cmpcld 23411 | . . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝑠) ∈ Comp ∧ (𝑠 ∩ 𝐴) ∈ (Clsd‘(𝐽 ↾t 𝑠))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) | 
| 66 | 51, 64, 65 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝑠) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) | 
| 67 | 50, 66 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) | 
| 68 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑣 = (𝑠 ∩ 𝐴) → ((𝐽 ↾t 𝐴) ↾t 𝑣) = ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴))) | 
| 69 | 68 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑣 = (𝑠 ∩ 𝐴) → (((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp)) | 
| 70 | 69 | rspcev 3621 | . . . . . . . . . . . 12
⊢ (((𝑠 ∩ 𝐴) ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴)) ∧ ((𝐽 ↾t 𝐴) ↾t (𝑠 ∩ 𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 71 | 42, 67, 70 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 72 | 71 | expr 456 | . . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢 ∧ 𝑤 ∈ 𝐽)) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 73 | 72 | rexlimdvva 3212 | . . . . . . . . 9
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → (∃𝑠 ∈ 𝒫 𝑢∃𝑤 ∈ 𝐽 (𝑦 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 74 | 10, 73 | mpd 15 | . . . . . . . 8
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧
(𝑢 ∈ 𝐽 ∧ 𝑦 ∈ (𝑢 ∩ 𝐴))) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 75 | 74 | anassrs 467 | . . . . . . 7
⊢ ((((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝑢 ∩ 𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 76 | 75 | ralrimiva 3145 | . . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 77 |  | pweq 4613 | . . . . . . . . 9
⊢ (𝑥 = (𝑢 ∩ 𝐴) → 𝒫 𝑥 = 𝒫 (𝑢 ∩ 𝐴)) | 
| 78 | 77 | ineq2d 4219 | . . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))) | 
| 79 | 78 | rexeqdv 3326 | . . . . . . 7
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 80 | 79 | raleqbi1dv 3337 | . . . . . 6
⊢ (𝑥 = (𝑢 ∩ 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢 ∩ 𝐴)∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢 ∩ 𝐴))((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 81 | 76, 80 | syl5ibrcom 247 | . . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 82 | 81 | rexlimdva 3154 | . . . 4
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 83 | 4, 82 | sylbid 240 | . . 3
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝑥 ∈ (𝐽 ↾t 𝐴) → ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 84 | 83 | ralrimiv 3144 | . 2
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
∀𝑥 ∈ (𝐽 ↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp) | 
| 85 |  | isnlly 23478 | . 2
⊢ ((𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp
↔ ((𝐽
↾t 𝐴)
∈ Top ∧ ∀𝑥
∈ (𝐽
↾t 𝐴)∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽 ↾t 𝐴) ↾t 𝑣) ∈ Comp)) | 
| 86 | 3, 84, 85 | sylanbrc 583 | 1
⊢ ((𝐽 ∈ 𝑛-Locally Comp
∧ 𝐴 ∈
(Clsd‘𝐽)) →
(𝐽 ↾t
𝐴) ∈ 𝑛-Locally
Comp) |