| Step | Hyp | Ref
| Expression |
| 1 | | restlly.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ Top) |
| 2 | 1 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ Top) |
| 3 | | simprl 771 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝑗) |
| 4 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 5 | 4 | pwid 4622 |
. . . . . . . 8
⊢ 𝑥 ∈ 𝒫 𝑥 |
| 6 | 5 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝑥) |
| 7 | 3, 6 | elind 4200 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → 𝑥 ∈ (𝑗 ∩ 𝒫 𝑥)) |
| 8 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → 𝑦 ∈ 𝑥) |
| 9 | | restlly.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) |
| 10 | 9 | anassrs 467 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 ∈ 𝑗) → (𝑗 ↾t 𝑥) ∈ 𝐴) |
| 11 | 10 | adantrr 717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → (𝑗 ↾t 𝑥) ∈ 𝐴) |
| 12 | | elequ2 2123 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑥)) |
| 13 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑢 = 𝑥 → (𝑗 ↾t 𝑢) = (𝑗 ↾t 𝑥)) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → ((𝑗 ↾t 𝑢) ∈ 𝐴 ↔ (𝑗 ↾t 𝑥) ∈ 𝐴)) |
| 15 | 12, 14 | anbi12d 632 |
. . . . . . 7
⊢ (𝑢 = 𝑥 → ((𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴) ↔ (𝑦 ∈ 𝑥 ∧ (𝑗 ↾t 𝑥) ∈ 𝐴))) |
| 16 | 15 | rspcev 3622 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑗 ∩ 𝒫 𝑥) ∧ (𝑦 ∈ 𝑥 ∧ (𝑗 ↾t 𝑥) ∈ 𝐴)) → ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)) |
| 17 | 7, 8, 11, 16 | syl12anc 837 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ (𝑥 ∈ 𝑗 ∧ 𝑦 ∈ 𝑥)) → ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)) |
| 18 | 17 | ralrimivva 3202 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)) |
| 19 | | islly 23476 |
. . . 4
⊢ (𝑗 ∈ Locally 𝐴 ↔ (𝑗 ∈ Top ∧ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴))) |
| 20 | 2, 18, 19 | sylanbrc 583 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ Locally 𝐴) |
| 21 | 20 | ex 412 |
. 2
⊢ (𝜑 → (𝑗 ∈ 𝐴 → 𝑗 ∈ Locally 𝐴)) |
| 22 | 21 | ssrdv 3989 |
1
⊢ (𝜑 → 𝐴 ⊆ Locally 𝐴) |