Proof of Theorem nlly2i
Step | Hyp | Ref
| Expression |
1 | | nllyi 21088 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ ((nei‘𝐽)‘{𝑃})(𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) |
2 | | simprrl 800 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → 𝑠 ⊆ 𝑈) |
3 | | selpw 4115 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝑈 ↔ 𝑠 ⊆ 𝑈) |
4 | 2, 3 | sylibr 223 |
. . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → 𝑠 ∈ 𝒫 𝑈) |
5 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → 𝐽 ∈ 𝑛-Locally 𝐴) |
6 | | nllytop 21086 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → 𝐽 ∈ Top) |
8 | | simprl 790 |
. . . . . . 7
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → 𝑠 ∈ ((nei‘𝐽)‘{𝑃})) |
9 | | neii2 20722 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑠 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑢 ∈ 𝐽 ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) |
10 | 7, 8, 9 | syl2anc 691 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → ∃𝑢 ∈ 𝐽 ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) |
11 | | simprl 790 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → {𝑃} ⊆ 𝑢) |
12 | | simpll3 1095 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → 𝑃 ∈ 𝑈) |
13 | | snssg 4268 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ 𝑈 → (𝑃 ∈ 𝑢 ↔ {𝑃} ⊆ 𝑢)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → (𝑃 ∈ 𝑢 ↔ {𝑃} ⊆ 𝑢)) |
15 | 11, 14 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → 𝑃 ∈ 𝑢) |
16 | | simprr 792 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ 𝑠) |
17 | | simprrr 801 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → (𝐽 ↾t 𝑠) ∈ 𝐴) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → (𝐽 ↾t 𝑠) ∈ 𝐴) |
19 | 15, 16, 18 | 3jca 1235 |
. . . . . . . 8
⊢ ((((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) ∧ ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠)) → (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) |
20 | 19 | ex 449 |
. . . . . . 7
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → (({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠) → (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) |
21 | 20 | reximdv 2999 |
. . . . . 6
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → (∃𝑢 ∈ 𝐽 ({𝑃} ⊆ 𝑢 ∧ 𝑢 ⊆ 𝑠) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) |
22 | 10, 21 | mpd 15 |
. . . . 5
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) |
23 | 4, 22 | jca 553 |
. . . 4
⊢ (((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) ∧ (𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) → (𝑠 ∈ 𝒫 𝑈 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) |
24 | 23 | ex 449 |
. . 3
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ((𝑠 ∈ ((nei‘𝐽)‘{𝑃}) ∧ (𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) → (𝑠 ∈ 𝒫 𝑈 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)))) |
25 | 24 | reximdv2 2997 |
. 2
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → (∃𝑠 ∈ ((nei‘𝐽)‘{𝑃})(𝑠 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))) |
26 | 1, 25 | mpd 15 |
1
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) |