Metamath Proof Explorer

Theorem nllyi

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

Ref Expression
Assertion nllyi ⊢ J ∈ N-Locally A ∧ U ∈ J ∧ P ∈ U → ∃ u ∈ nei ⁡ J ⁡ P u ⊆ U ∧ J ↾ 𝑡 u ∈ A

Proof

Step Hyp Ref Expression
1 isnlly ⊢ J ∈ N-Locally A ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
2 1 simprbi ⊢ J ∈ N-Locally A → ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
3 pweq ⊢ x = U → 𝒫 x = 𝒫 U
4 3 ineq2d ⊢ x = U → nei ⁡ J ⁡ y ∩ 𝒫 x = nei ⁡ J ⁡ y ∩ 𝒫 U
5 4 rexeqdv ⊢ x = U → ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A ↔ ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A
6 5 raleqbi1dv ⊢ x = U → ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A ↔ ∀ y ∈ U ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A
7 6 rspccva ⊢ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A ∧ U ∈ J → ∀ y ∈ U ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A
8 2 7 sylan ⊢ J ∈ N-Locally A ∧ U ∈ J → ∀ y ∈ U ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A
9 elin ⊢ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U ↔ u ∈ nei ⁡ J ⁡ y ∧ u ∈ 𝒫 U
10 sneq ⊢ y = P → y = P
11 10 fveq2d ⊢ y = P → nei ⁡ J ⁡ y = nei ⁡ J ⁡ P
12 11 eleq2d ⊢ y = P → u ∈ nei ⁡ J ⁡ y ↔ u ∈ nei ⁡ J ⁡ P
13 velpw ⊢ u ∈ 𝒫 U ↔ u ⊆ U
14 13 a1i ⊢ y = P → u ∈ 𝒫 U ↔ u ⊆ U
15 12 14 anbi12d ⊢ y = P → u ∈ nei ⁡ J ⁡ y ∧ u ∈ 𝒫 U ↔ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U
16 9 15 syl5bb ⊢ y = P → u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U ↔ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U
17 16 anbi1d ⊢ y = P → u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U ∧ J ↾ 𝑡 u ∈ A ↔ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U ∧ J ↾ 𝑡 u ∈ A
18 anass ⊢ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U ∧ J ↾ 𝑡 u ∈ A ↔ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U ∧ J ↾ 𝑡 u ∈ A
19 17 18 bitrdi ⊢ y = P → u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U ∧ J ↾ 𝑡 u ∈ A ↔ u ∈ nei ⁡ J ⁡ P ∧ u ⊆ U ∧ J ↾ 𝑡 u ∈ A
20 19 rexbidv2 ⊢ y = P → ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A ↔ ∃ u ∈ nei ⁡ J ⁡ P u ⊆ U ∧ J ↾ 𝑡 u ∈ A
21 20 rspccva ⊢ ∀ y ∈ U ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 U J ↾ 𝑡 u ∈ A ∧ P ∈ U → ∃ u ∈ nei ⁡ J ⁡ P u ⊆ U ∧ J ↾ 𝑡 u ∈ A
22 8 21 stoic3 ⊢ J ∈ N-Locally A ∧ U ∈ J ∧ P ∈ U → ∃ u ∈ nei ⁡ J ⁡ P u ⊆ U ∧ J ↾ 𝑡 u ∈ A