Step |
Hyp |
Ref |
Expression |
1 |
|
restlly.1 |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) |
2 |
|
nllytop |
⊢ ( 𝑘 ∈ 𝑛-Locally 𝐴 → 𝑘 ∈ Top ) |
3 |
2
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) → 𝑘 ∈ Top ) |
4 |
|
nlly2i |
⊢ ( ( 𝑘 ∈ 𝑛-Locally 𝐴 ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) → ∃ 𝑠 ∈ 𝒫 𝑦 ∃ 𝑥 ∈ 𝑘 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) |
5 |
4
|
3adant1l |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) → ∃ 𝑠 ∈ 𝒫 𝑦 ∃ 𝑥 ∈ 𝑘 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) |
6 |
|
simprl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ 𝑘 ) |
7 |
|
simprr2 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ⊆ 𝑠 ) |
8 |
|
simplr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝒫 𝑦 ) |
9 |
8
|
elpwid |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑦 ) |
10 |
7 9
|
sstrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ⊆ 𝑦 ) |
11 |
|
velpw |
⊢ ( 𝑥 ∈ 𝒫 𝑦 ↔ 𝑥 ⊆ 𝑦 ) |
12 |
10 11
|
sylibr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ 𝒫 𝑦 ) |
13 |
6 12
|
elind |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ) |
14 |
|
simprr1 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝑥 ) |
15 |
|
simpll1 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ) |
16 |
15 2
|
simpl2im |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑘 ∈ Top ) |
17 |
|
restabs |
⊢ ( ( 𝑘 ∈ Top ∧ 𝑥 ⊆ 𝑠 ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) = ( 𝑘 ↾t 𝑥 ) ) |
18 |
16 7 8 17
|
syl3anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) = ( 𝑘 ↾t 𝑥 ) ) |
19 |
|
df-ss |
⊢ ( 𝑥 ⊆ 𝑠 ↔ ( 𝑥 ∩ 𝑠 ) = 𝑥 ) |
20 |
7 19
|
sylib |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∩ 𝑠 ) = 𝑥 ) |
21 |
|
elrestr |
⊢ ( ( 𝑘 ∈ Top ∧ 𝑠 ∈ 𝒫 𝑦 ∧ 𝑥 ∈ 𝑘 ) → ( 𝑥 ∩ 𝑠 ) ∈ ( 𝑘 ↾t 𝑠 ) ) |
22 |
16 8 6 21
|
syl3anc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∩ 𝑠 ) ∈ ( 𝑘 ↾t 𝑠 ) ) |
23 |
20 22
|
eqeltrrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑥 ∈ ( 𝑘 ↾t 𝑠 ) ) |
24 |
|
eleq2 |
⊢ ( 𝑗 = ( 𝑘 ↾t 𝑠 ) → ( 𝑥 ∈ 𝑗 ↔ 𝑥 ∈ ( 𝑘 ↾t 𝑠 ) ) ) |
25 |
|
oveq1 |
⊢ ( 𝑗 = ( 𝑘 ↾t 𝑠 ) → ( 𝑗 ↾t 𝑥 ) = ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) ) |
26 |
25
|
eleq1d |
⊢ ( 𝑗 = ( 𝑘 ↾t 𝑠 ) → ( ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ↔ ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) ) |
27 |
24 26
|
imbi12d |
⊢ ( 𝑗 = ( 𝑘 ↾t 𝑠 ) → ( ( 𝑥 ∈ 𝑗 → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ↔ ( 𝑥 ∈ ( 𝑘 ↾t 𝑠 ) → ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
28 |
15
|
simpld |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → 𝜑 ) |
29 |
1
|
expr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑗 → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) |
30 |
29
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ( 𝑥 ∈ 𝑗 → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) |
31 |
28 30
|
syl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ∀ 𝑗 ∈ 𝐴 ( 𝑥 ∈ 𝑗 → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) |
32 |
|
simprr3 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) |
33 |
27 31 32
|
rspcdva |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝑘 ↾t 𝑠 ) → ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) ) |
34 |
23 33
|
mpd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑘 ↾t 𝑠 ) ↾t 𝑥 ) ∈ 𝐴 ) |
35 |
18 34
|
eqeltrrd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) |
36 |
13 14 35
|
jca32 |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) ∧ ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ∧ ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
37 |
36
|
ex |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ( 𝑥 ∈ 𝑘 ∧ ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ∧ ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) ) ) |
38 |
37
|
reximdv2 |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ∧ 𝑠 ∈ 𝒫 𝑦 ) → ( ∃ 𝑥 ∈ 𝑘 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
39 |
38
|
rexlimdva |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) → ( ∃ 𝑠 ∈ 𝒫 𝑦 ∃ 𝑥 ∈ 𝑘 ( 𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ 𝑠 ∧ ( 𝑘 ↾t 𝑠 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
40 |
5 39
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) |
41 |
40
|
3expb |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) ∧ ( 𝑦 ∈ 𝑘 ∧ 𝑢 ∈ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) |
42 |
41
|
ralrimivva |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) → ∀ 𝑦 ∈ 𝑘 ∀ 𝑢 ∈ 𝑦 ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) |
43 |
|
islly |
⊢ ( 𝑘 ∈ Locally 𝐴 ↔ ( 𝑘 ∈ Top ∧ ∀ 𝑦 ∈ 𝑘 ∀ 𝑢 ∈ 𝑦 ∃ 𝑥 ∈ ( 𝑘 ∩ 𝒫 𝑦 ) ( 𝑢 ∈ 𝑥 ∧ ( 𝑘 ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
44 |
3 42 43
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑛-Locally 𝐴 ) → 𝑘 ∈ Locally 𝐴 ) |
45 |
44
|
ex |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝑛-Locally 𝐴 → 𝑘 ∈ Locally 𝐴 ) ) |
46 |
45
|
ssrdv |
⊢ ( 𝜑 → 𝑛-Locally 𝐴 ⊆ Locally 𝐴 ) |
47 |
|
llyssnlly |
⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴 |
48 |
47
|
a1i |
⊢ ( 𝜑 → Locally 𝐴 ⊆ 𝑛-Locally 𝐴 ) |
49 |
46 48
|
eqssd |
⊢ ( 𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴 ) |