MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cldllycmp Structured version   Visualization version   GIF version

Theorem cldllycmp 23504
Description: A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 23495.) (Contributed by Mario Carneiro, 2-Mar-2015.)
Assertion
Ref Expression
cldllycmp ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ 𝑛-Locally Comp)

Proof of Theorem cldllycmp
Dummy variables 𝑢 𝑣 𝑤 𝑥 𝑦 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nllytop 23482 . . 3 (𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ Top)
2 resttop 23169 . . 3 ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
31, 2sylan 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‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → 𝑦 ∈ (𝑢𝐴))
87elin1d 4203 . . . . . . . . . 10 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → 𝑦𝑢)
9 nlly2i 23485 . . . . . . . . . 10 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝑢𝐽𝑦𝑢) → ∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))
105, 6, 8, 9syl3anc 1372 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → ∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))
113ad2antrr 726 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝐽t 𝐴) ∈ Top)
121ad3antrrr 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 𝐴))
1612, 13, 14, 15syl3anc 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))) → 𝑦 ∈ (𝑢𝐴))
1918elin2d 4204 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦𝐴)
2017, 19elind 4199 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤𝐴))
21 opnneip 23128 . . . . . . . . . . . . . . 15 (((𝐽t 𝐴) ∈ Top ∧ (𝑤𝐴) ∈ (𝐽t 𝐴) ∧ 𝑦 ∈ (𝑤𝐴)) → (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
2211, 16, 20, 21syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
23 simprr2 1222 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑤𝑠)
2423ssrind 4243 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑤𝐴) ⊆ (𝑠𝐴))
25 inss2 4237 . . . . . . . . . . . . . . 15 (𝑠𝐴) ⊆ 𝐴
26 eqid 2736 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
2726cldss 23038 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (Clsd‘𝐽) → 𝐴 𝐽)
2813, 27syl 17 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝐴 𝐽)
2926restuni 23171 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴 𝐽) → 𝐴 = (𝐽t 𝐴))
3012, 28, 29syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝐴 = (𝐽t 𝐴))
3125, 30sseqtrid 4025 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ (𝐽t 𝐴))
32 eqid 2736 . . . . . . . . . . . . . . 15 (𝐽t 𝐴) = (𝐽t 𝐴)
3332ssnei2 23125 . . . . . . . . . . . . . 14 ((((𝐽t 𝐴) ∈ Top ∧ (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦})) ∧ ((𝑤𝐴) ⊆ (𝑠𝐴) ∧ (𝑠𝐴) ⊆ (𝐽t 𝐴))) → (𝑠𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
3411, 22, 24, 31, 33syl22anc 838 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
35 simprll 778 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢)
3635elpwid 4608 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠𝑢)
3736ssrind 4243 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ (𝑢𝐴))
38 vex 3483 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
3938inex1 5316 . . . . . . . . . . . . . . 15 (𝑠𝐴) ∈ V
4039elpw 4603 . . . . . . . . . . . . . 14 ((𝑠𝐴) ∈ 𝒫 (𝑢𝐴) ↔ (𝑠𝐴) ⊆ (𝑢𝐴))
4137, 40sylibr 234 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ 𝒫 (𝑢𝐴))
4234, 41elind 4199 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)))
4325a1i 11 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ 𝐴)
44 restabs 23174 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ (𝑠𝐴) ⊆ 𝐴𝐴 ∈ (Clsd‘𝐽)) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
4512, 43, 13, 44syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
46 inss1 4236 . . . . . . . . . . . . . . . 16 (𝑠𝐴) ⊆ 𝑠
4746a1i 11 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ 𝑠)
48 restabs 23174 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ (𝑠𝐴) ⊆ 𝑠𝑠 ∈ 𝒫 𝑢) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
4912, 47, 35, 48syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
5045, 49eqtr4d 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 (𝑣 = 𝐴 → (𝑣𝑠) = (𝐴𝑠))
5554rspceeqv 3644 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴𝑠) = (𝐴𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠))
5613, 53, 55sylancl 586 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠))
57 simplrl 776 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑢𝐽)
58 elssuni 4936 . . . . . . . . . . . . . . . . . . 19 (𝑢𝐽𝑢 𝐽)
5957, 58syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑢 𝐽)
6036, 59sstrd 3993 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠 𝐽)
6126restcld 23181 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑠 𝐽) → ((𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠)))
6212, 60, 61syl2anc 584 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠)))
6356, 62mpbird 257 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)))
6452, 63eqeltrid 2844 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ (Clsd‘(𝐽t 𝑠)))
65 cmpcld 23411 . . . . . . . . . . . . . 14 (((𝐽t 𝑠) ∈ Comp ∧ (𝑠𝐴) ∈ (Clsd‘(𝐽t 𝑠))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) ∈ Comp)
6651, 64, 65syl2anc 584 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) ∈ Comp)
6750, 66eqeltrd 2840 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp)
68 oveq2 7440 . . . . . . . . . . . . . 14 (𝑣 = (𝑠𝐴) → ((𝐽t 𝐴) ↾t 𝑣) = ((𝐽t 𝐴) ↾t (𝑠𝐴)))
6968eleq1d 2825 . . . . . . . . . . . . 13 (𝑣 = (𝑠𝐴) → (((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp))
7069rspcev 3621 . . . . . . . . . . . 12 (((𝑠𝐴) ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)) ∧ ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7142, 67, 70syl2anc 584 . . . . . . . . . . 11 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7271expr 456 . . . . . . . . . 10 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢𝑤𝐽)) → ((𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
7372rexlimdvva 3212 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → (∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
7410, 73mpd 15 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7574anassrs 467 . . . . . . 7 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) ∧ 𝑦 ∈ (𝑢𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7675ralrimiva 3145 . . . . . 6 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝐴)∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
77 pweq 4613 . . . . . . . . 9 (𝑥 = (𝑢𝐴) → 𝒫 𝑥 = 𝒫 (𝑢𝐴))
7877ineq2d 4219 . . . . . . . 8 (𝑥 = (𝑢𝐴) → (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)))
7978rexeqdv 3326 . . . . . . 7 (𝑥 = (𝑢𝐴) → (∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8079raleqbi1dv 3337 . . . . . 6 (𝑥 = (𝑢𝐴) → (∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢𝐴)∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8176, 80syl5ibrcom 247 . . . . 5 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) → (𝑥 = (𝑢𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8281rexlimdva 3154 . . . 4 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (∃𝑢𝐽 𝑥 = (𝑢𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
834, 82sylbid 240 . . 3 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ (𝐽t 𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8483ralrimiv 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))
863, 84, 85sylanbrc 583 1 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ 𝑛-Locally Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wral 3060  wrex 3069  cin 3949  wss 3950  𝒫 cpw 4599  {csn 4625   cuni 4906  cfv 6560  (class class class)co 7432  t crest 17466  Topctop 22900  Clsdccld 23025  neicnei 23106  Compccmp 23395  𝑛-Locally cnlly 23474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-1o 8507  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-rest 17468  df-topgen 17489  df-top 22901  df-topon 22918  df-bases 22954  df-cld 23028  df-nei 23107  df-cmp 23396  df-nlly 23476
This theorem is referenced by:  rellycmp  24990
  Copyright terms: Public domain W3C validator