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

Theorem cldllycmp 22098
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 22089.) (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 22076 . . 3 (𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ Top)
2 resttop 21763 . . 3 ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
31, 2sylan 583 . 2 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ Top)
4 elrest 16692 . . . 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 4149 . . . . . . . . . 10 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → 𝑦𝑢)
9 nlly2i 22079 . . . . . . . . . 10 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝑢𝐽𝑦𝑢) → ∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))
105, 6, 8, 9syl3anc 1368 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → ∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))
113ad2antrr 725 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝐽t 𝐴) ∈ Top)
121ad3antrrr 729 . . . . . . . . . . . . . . . 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 16693 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴 ∈ (Clsd‘𝐽) ∧ 𝑤𝐽) → (𝑤𝐴) ∈ (𝐽t 𝐴))
1612, 13, 14, 15syl3anc 1368 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑤𝐴) ∈ (𝐽t 𝐴))
17 simprr1 1218 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦𝑤)
18 simplrr 777 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑢𝐴))
1918elin2d 4150 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦𝐴)
2017, 19elind 4145 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑦 ∈ (𝑤𝐴))
21 opnneip 21722 . . . . . . . . . . . . . . 15 (((𝐽t 𝐴) ∈ Top ∧ (𝑤𝐴) ∈ (𝐽t 𝐴) ∧ 𝑦 ∈ (𝑤𝐴)) → (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
2211, 16, 20, 21syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
23 simprr2 1219 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑤𝑠)
2423ssrind 4186 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑤𝐴) ⊆ (𝑠𝐴))
25 inss2 4180 . . . . . . . . . . . . . . 15 (𝑠𝐴) ⊆ 𝐴
26 eqid 2822 . . . . . . . . . . . . . . . . . 18 𝐽 = 𝐽
2726cldss 21632 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (Clsd‘𝐽) → 𝐴 𝐽)
2813, 27syl 17 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝐴 𝐽)
2926restuni 21765 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝐴 𝐽) → 𝐴 = (𝐽t 𝐴))
3012, 28, 29syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝐴 = (𝐽t 𝐴))
3125, 30sseqtrid 3994 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ (𝐽t 𝐴))
32 eqid 2822 . . . . . . . . . . . . . . 15 (𝐽t 𝐴) = (𝐽t 𝐴)
3332ssnei2 21719 . . . . . . . . . . . . . 14 ((((𝐽t 𝐴) ∈ Top ∧ (𝑤𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦})) ∧ ((𝑤𝐴) ⊆ (𝑠𝐴) ∧ (𝑠𝐴) ⊆ (𝐽t 𝐴))) → (𝑠𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
3411, 22, 24, 31, 33syl22anc 837 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ ((nei‘(𝐽t 𝐴))‘{𝑦}))
35 simprll 778 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠 ∈ 𝒫 𝑢)
3635elpwid 4522 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠𝑢)
3736ssrind 4186 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ (𝑢𝐴))
38 vex 3472 . . . . . . . . . . . . . . . 16 𝑠 ∈ V
3938inex1 5197 . . . . . . . . . . . . . . 15 (𝑠𝐴) ∈ V
4039elpw 4515 . . . . . . . . . . . . . 14 ((𝑠𝐴) ∈ 𝒫 (𝑢𝐴) ↔ (𝑠𝐴) ⊆ (𝑢𝐴))
4137, 40sylibr 237 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ 𝒫 (𝑢𝐴))
4234, 41elind 4145 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)))
4325a1i 11 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ 𝐴)
44 restabs 21768 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ (𝑠𝐴) ⊆ 𝐴𝐴 ∈ (Clsd‘𝐽)) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
4512, 43, 13, 44syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
46 inss1 4179 . . . . . . . . . . . . . . . 16 (𝑠𝐴) ⊆ 𝑠
4746a1i 11 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ⊆ 𝑠)
48 restabs 21768 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ (𝑠𝐴) ⊆ 𝑠𝑠 ∈ 𝒫 𝑢) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
4912, 47, 35, 48syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) = (𝐽t (𝑠𝐴)))
5045, 49eqtr4d 2860 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) = ((𝐽t 𝑠) ↾t (𝑠𝐴)))
51 simprr3 1220 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝐽t 𝑠) ∈ Comp)
52 incom 4152 . . . . . . . . . . . . . . 15 (𝑠𝐴) = (𝐴𝑠)
53 eqid 2822 . . . . . . . . . . . . . . . . 17 (𝐴𝑠) = (𝐴𝑠)
54 ineq1 4155 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝐴 → (𝑣𝑠) = (𝐴𝑠))
5554rspceeqv 3613 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ (Clsd‘𝐽) ∧ (𝐴𝑠) = (𝐴𝑠)) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠))
5613, 53, 55sylancl 589 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠))
57 simplrl 776 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑢𝐽)
58 elssuni 4843 . . . . . . . . . . . . . . . . . . 19 (𝑢𝐽𝑢 𝐽)
5957, 58syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑢 𝐽)
6036, 59sstrd 3952 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → 𝑠 𝐽)
6126restcld 21775 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑠 𝐽) → ((𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠)))
6212, 60, 61syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)) ↔ ∃𝑣 ∈ (Clsd‘𝐽)(𝐴𝑠) = (𝑣𝑠)))
6356, 62mpbird 260 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝐴𝑠) ∈ (Clsd‘(𝐽t 𝑠)))
6452, 63eqeltrid 2918 . . . . . . . . . . . . . 14 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → (𝑠𝐴) ∈ (Clsd‘(𝐽t 𝑠)))
65 cmpcld 22005 . . . . . . . . . . . . . 14 (((𝐽t 𝑠) ∈ Comp ∧ (𝑠𝐴) ∈ (Clsd‘(𝐽t 𝑠))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) ∈ Comp)
6651, 64, 65syl2anc 587 . . . . . . . . . . . . 13 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝑠) ↾t (𝑠𝐴)) ∈ Comp)
6750, 66eqeltrd 2914 . . . . . . . . . . . 12 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp)
68 oveq2 7148 . . . . . . . . . . . . . 14 (𝑣 = (𝑠𝐴) → ((𝐽t 𝐴) ↾t 𝑣) = ((𝐽t 𝐴) ↾t (𝑠𝐴)))
6968eleq1d 2898 . . . . . . . . . . . . 13 (𝑣 = (𝑠𝐴) → (((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp))
7069rspcev 3598 . . . . . . . . . . . 12 (((𝑠𝐴) ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)) ∧ ((𝐽t 𝐴) ↾t (𝑠𝐴)) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7142, 67, 70syl2anc 587 . . . . . . . . . . 11 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ ((𝑠 ∈ 𝒫 𝑢𝑤𝐽) ∧ (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp))) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7271expr 460 . . . . . . . . . 10 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) ∧ (𝑠 ∈ 𝒫 𝑢𝑤𝐽)) → ((𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
7372rexlimdvva 3280 . . . . . . . . 9 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → (∃𝑠 ∈ 𝒫 𝑢𝑤𝐽 (𝑦𝑤𝑤𝑠 ∧ (𝐽t 𝑠) ∈ Comp) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
7410, 73mpd 15 . . . . . . . 8 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ (𝑢𝐽𝑦 ∈ (𝑢𝐴))) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7574anassrs 471 . . . . . . 7 ((((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) ∧ 𝑦 ∈ (𝑢𝐴)) → ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
7675ralrimiva 3174 . . . . . 6 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝐴)∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
77 pweq 4527 . . . . . . . . 9 (𝑥 = (𝑢𝐴) → 𝒫 𝑥 = 𝒫 (𝑢𝐴))
7877ineq2d 4163 . . . . . . . 8 (𝑥 = (𝑢𝐴) → (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥) = (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴)))
7978rexeqdv 3393 . . . . . . 7 (𝑥 = (𝑢𝐴) → (∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8079raleqbi1dv 3384 . . . . . 6 (𝑥 = (𝑢𝐴) → (∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp ↔ ∀𝑦 ∈ (𝑢𝐴)∃𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 (𝑢𝐴))((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8176, 80syl5ibrcom 250 . . . . 5 (((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) ∧ 𝑢𝐽) → (𝑥 = (𝑢𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8281rexlimdva 3270 . . . 4 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (∃𝑢𝐽 𝑥 = (𝑢𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
834, 82sylbid 243 . . 3 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝑥 ∈ (𝐽t 𝐴) → ∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
8483ralrimiv 3173 . 2 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → ∀𝑥 ∈ (𝐽t 𝐴)∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp)
85 isnlly 22072 . 2 ((𝐽t 𝐴) ∈ 𝑛-Locally Comp ↔ ((𝐽t 𝐴) ∈ Top ∧ ∀𝑥 ∈ (𝐽t 𝐴)∀𝑦𝑥𝑣 ∈ (((nei‘(𝐽t 𝐴))‘{𝑦}) ∩ 𝒫 𝑥)((𝐽t 𝐴) ↾t 𝑣) ∈ Comp))
863, 84, 85sylanbrc 586 1 ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽t 𝐴) ∈ 𝑛-Locally Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wral 3130  wrex 3131  cin 3907  wss 3908  𝒫 cpw 4511  {csn 4539   cuni 4813  cfv 6334  (class class class)co 7140  t crest 16685  Topctop 21496  Clsdccld 21619  neicnei 21700  Compccmp 21989  𝑛-Locally cnlly 22068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-fin 8500  df-fi 8863  df-rest 16687  df-topgen 16708  df-top 21497  df-topon 21514  df-bases 21549  df-cld 21622  df-nei 21701  df-cmp 21990  df-nlly 22070
This theorem is referenced by:  rellycmp  23560
  Copyright terms: Public domain W3C validator