Metamath Proof Explorer

Theorem isnlly

Description: The property of being an n-locally A topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion isnlly ⊢ J ∈ N-Locally A ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ j = J → nei ⁡ j = nei ⁡ J
2 1 fveq1d ⊢ j = J → nei ⁡ j ⁡ y = nei ⁡ J ⁡ y
3 2 ineq1d ⊢ j = J → nei ⁡ j ⁡ y ∩ 𝒫 x = nei ⁡ J ⁡ y ∩ 𝒫 x
4 oveq1 ⊢ j = J → j ↾ 𝑡 u = J ↾ 𝑡 u
5 4 eleq1d ⊢ j = J → j ↾ 𝑡 u ∈ A ↔ J ↾ 𝑡 u ∈ A
6 3 5 rexeqbidv ⊢ j = J → ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A ↔ ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
7 6 ralbidv ⊢ j = J → ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A ↔ ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
8 7 raleqbi1dv ⊢ j = J → ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A ↔ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
9 df-nlly ⊢ N-Locally A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
10 8 9 elrab2 ⊢ J ∈ N-Locally A ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A