Step |
Hyp |
Ref |
Expression |
1 |
|
restlly.1 |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) |
2 |
|
restlly.2 |
⊢ ( 𝜑 → 𝐴 ⊆ Top ) |
3 |
2
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ Top ) |
4 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝑗 ) |
5 |
|
vex |
⊢ 𝑥 ∈ V |
6 |
5
|
pwid |
⊢ 𝑥 ∈ 𝒫 𝑥 |
7 |
6
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝒫 𝑥 ) |
8 |
4 7
|
elind |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ) |
9 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑥 ) |
10 |
1
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) |
11 |
10
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) |
12 |
|
elequ2 |
⊢ ( 𝑢 = 𝑥 → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑥 ) ) |
13 |
|
oveq2 |
⊢ ( 𝑢 = 𝑥 → ( 𝑗 ↾t 𝑢 ) = ( 𝑗 ↾t 𝑥 ) ) |
14 |
13
|
eleq1d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) |
15 |
12 14
|
anbi12d |
⊢ ( 𝑢 = 𝑥 → ( ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) ) |
16 |
15
|
rspcev |
⊢ ( ( 𝑥 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ 𝑥 ∧ ( 𝑗 ↾t 𝑥 ) ∈ 𝐴 ) ) → ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ) |
17 |
8 9 11 16
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥 ) ) → ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ) |
18 |
17
|
ralrimivva |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ) |
19 |
|
islly |
⊢ ( 𝑗 ∈ Locally 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝑗 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ) ) ) |
20 |
3 18 19
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ Locally 𝐴 ) |
21 |
20
|
ex |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 → 𝑗 ∈ Locally 𝐴 ) ) |
22 |
21
|
ssrdv |
⊢ ( 𝜑 → 𝐴 ⊆ Locally 𝐴 ) |