Step | Hyp | Ref
| Expression |
1 | | llytop 21085 |
. . . 4
⊢ (𝑗 ∈ Locally
𝑛-Locally 𝐴 →
𝑗 ∈
Top) |
2 | | llyi 21087 |
. . . . . . 7
⊢ ((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) → ∃𝑢 ∈ 𝑗 (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴)) |
3 | | simprr3 1104 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴) |
4 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑢 ∈ 𝑗) |
5 | | ssid 3587 |
. . . . . . . . . . 11
⊢ 𝑢 ⊆ 𝑢 |
6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑢 ⊆ 𝑢) |
7 | | simpl1 1057 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑗 ∈ Locally 𝑛-Locally 𝐴) |
8 | 7, 1 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑗 ∈ Top) |
9 | | restopn2 20791 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗) → (𝑢 ∈ (𝑗 ↾t 𝑢) ↔ (𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢))) |
10 | 8, 4, 9 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → (𝑢 ∈ (𝑗 ↾t 𝑢) ↔ (𝑢 ∈ 𝑗 ∧ 𝑢 ⊆ 𝑢))) |
11 | 4, 6, 10 | mpbir2and 959 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑢 ∈ (𝑗 ↾t 𝑢)) |
12 | | simprr2 1103 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑦 ∈ 𝑢) |
13 | | nlly2i 21089 |
. . . . . . . . 9
⊢ (((𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ (𝑗 ↾t 𝑢) ∧ 𝑦 ∈ 𝑢) → ∃𝑣 ∈ 𝒫 𝑢∃𝑧 ∈ (𝑗 ↾t 𝑢)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴)) |
14 | 3, 11, 12, 13 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → ∃𝑣 ∈ 𝒫 𝑢∃𝑧 ∈ (𝑗 ↾t 𝑢)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴)) |
15 | | restopn2 20791 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗) → (𝑧 ∈ (𝑗 ↾t 𝑢) ↔ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢))) |
16 | 8, 4, 15 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → (𝑧 ∈ (𝑗 ↾t 𝑢) ↔ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢))) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ 𝑣 ∈ 𝒫 𝑢) → (𝑧 ∈ (𝑗 ↾t 𝑢) ↔ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢))) |
18 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑗 ∈ Top) |
19 | | simpr2l 1113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑧 ∈ 𝑗) |
20 | | simpr31 1144 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑦 ∈ 𝑧) |
21 | | opnneip 20733 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ Top ∧ 𝑧 ∈ 𝑗 ∧ 𝑦 ∈ 𝑧) → 𝑧 ∈ ((nei‘𝑗)‘{𝑦})) |
22 | 18, 19, 20, 21 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑧 ∈ ((nei‘𝑗)‘{𝑦})) |
23 | | simpr32 1145 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑧 ⊆ 𝑣) |
24 | | simpr1 1060 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ∈ 𝒫 𝑢) |
25 | 24 | elpwid 4118 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ⊆ 𝑢) |
26 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑢 ∈ 𝑗) |
27 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ 𝑗 → 𝑢 ⊆ ∪ 𝑗) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑗) |
29 | 25, 28 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑗) |
30 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑗 =
∪ 𝑗 |
31 | 30 | ssnei2 20730 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 ∈ Top ∧ 𝑧 ∈ ((nei‘𝑗)‘{𝑦})) ∧ (𝑧 ⊆ 𝑣 ∧ 𝑣 ⊆ ∪ 𝑗)) → 𝑣 ∈ ((nei‘𝑗)‘{𝑦})) |
32 | 18, 22, 23, 29, 31 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ∈ ((nei‘𝑗)‘{𝑦})) |
33 | | simprr1 1102 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → 𝑢 ⊆ 𝑥) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑢 ⊆ 𝑥) |
35 | 25, 34 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ⊆ 𝑥) |
36 | | selpw 4115 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ 𝒫 𝑥 ↔ 𝑣 ⊆ 𝑥) |
37 | 35, 36 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ∈ 𝒫 𝑥) |
38 | 32, 37 | elind 3760 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → 𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)) |
39 | | restabs 20779 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ Top ∧ 𝑣 ⊆ 𝑢 ∧ 𝑢 ∈ 𝑗) → ((𝑗 ↾t 𝑢) ↾t 𝑣) = (𝑗 ↾t 𝑣)) |
40 | 18, 25, 26, 39 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → ((𝑗 ↾t 𝑢) ↾t 𝑣) = (𝑗 ↾t 𝑣)) |
41 | | simpr33 1146 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) |
42 | 40, 41 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → (𝑗 ↾t 𝑣) ∈ 𝐴) |
43 | 38, 42 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ (𝑣 ∈ 𝒫 𝑢 ∧ (𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴))) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴)) |
44 | 43 | 3exp2 1277 |
. . . . . . . . . . . . 13
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → (𝑣 ∈ 𝒫 𝑢 → ((𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴))))) |
45 | 44 | imp 444 |
. . . . . . . . . . . 12
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ 𝑣 ∈ 𝒫 𝑢) → ((𝑧 ∈ 𝑗 ∧ 𝑧 ⊆ 𝑢) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴)))) |
46 | 17, 45 | sylbid 229 |
. . . . . . . . . . 11
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ 𝑣 ∈ 𝒫 𝑢) → (𝑧 ∈ (𝑗 ↾t 𝑢) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴)))) |
47 | 46 | rexlimdv 3012 |
. . . . . . . . . 10
⊢ ((((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) ∧ 𝑣 ∈ 𝒫 𝑢) → (∃𝑧 ∈ (𝑗 ↾t 𝑢)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴))) |
48 | 47 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → ((𝑣 ∈ 𝒫 𝑢 ∧ ∃𝑧 ∈ (𝑗 ↾t 𝑢)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴)) → (𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥) ∧ (𝑗 ↾t 𝑣) ∈ 𝐴))) |
49 | 48 | reximdv2 2997 |
. . . . . . . 8
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → (∃𝑣 ∈ 𝒫 𝑢∃𝑧 ∈ (𝑗 ↾t 𝑢)(𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑣 ∧ ((𝑗 ↾t 𝑢) ↾t 𝑣) ∈ 𝐴) → ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴)) |
50 | 14, 49 | mpd 15 |
. . . . . . 7
⊢ (((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) ∧ (𝑢 ∈ 𝑗 ∧ (𝑢 ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝑛-Locally 𝐴))) → ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴) |
51 | 2, 50 | rexlimddv 3017 |
. . . . . 6
⊢ ((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥) → ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴) |
52 | 51 | 3expb 1258 |
. . . . 5
⊢ ((𝑗 ∈ Locally
𝑛-Locally 𝐴 ∧
(𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴) |
53 | 52 | ralrimivva 2954 |
. . . 4
⊢ (𝑗 ∈ Locally
𝑛-Locally 𝐴 →
∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴) |
54 | | isnlly 21082 |
. . . 4
⊢ (𝑗 ∈ 𝑛-Locally 𝐴 ↔ (𝑗 ∈ Top ∧ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑣 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑣) ∈ 𝐴)) |
55 | 1, 53, 54 | sylanbrc 695 |
. . 3
⊢ (𝑗 ∈ Locally
𝑛-Locally 𝐴 →
𝑗 ∈ 𝑛-Locally
𝐴) |
56 | 55 | ssriv 3572 |
. 2
⊢ Locally
𝑛-Locally 𝐴 ⊆
𝑛-Locally 𝐴 |
57 | | nllyrest 21099 |
. . . . 5
⊢ ((𝑗 ∈ 𝑛-Locally 𝐴 ∧ 𝑥 ∈ 𝑗) → (𝑗 ↾t 𝑥) ∈ 𝑛-Locally 𝐴) |
58 | 57 | adantl 481 |
. . . 4
⊢
((⊤ ∧ (𝑗
∈ 𝑛-Locally 𝐴
∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝑛-Locally 𝐴) |
59 | | nllytop 21086 |
. . . . . 6
⊢ (𝑗 ∈ 𝑛-Locally 𝐴 → 𝑗 ∈ Top) |
60 | 59 | ssriv 3572 |
. . . . 5
⊢
𝑛-Locally 𝐴
⊆ Top |
61 | 60 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝑛-Locally 𝐴
⊆ Top) |
62 | 58, 61 | restlly 21096 |
. . 3
⊢ (⊤
→ 𝑛-Locally 𝐴
⊆ Locally 𝑛-Locally 𝐴) |
63 | 62 | trud 1484 |
. 2
⊢
𝑛-Locally 𝐴
⊆ Locally 𝑛-Locally 𝐴 |
64 | 56, 63 | eqssi 3584 |
1
⊢ Locally
𝑛-Locally 𝐴 =
𝑛-Locally 𝐴 |