Metamath Proof Explorer

Theorem llynlly

Description: A locally A space is n-locally A : the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion llynlly ⊢ J ∈ Locally A → J ∈ N-Locally A

Proof

Step Hyp Ref Expression
1 llytop ⊢ J ∈ Locally A → J ∈ Top
2 llyi ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x → ∃ u ∈ J u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A
3 simpl1 ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → J ∈ Locally A
4 3 1 syl ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → J ∈ Top
5 simprl ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → u ∈ J
6 simprr2 ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → y ∈ u
7 opnneip ⊢ J ∈ Top ∧ u ∈ J ∧ y ∈ u → u ∈ nei ⁡ J ⁡ y
8 4 5 6 7 syl3anc ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → u ∈ nei ⁡ J ⁡ y
9 simprr1 ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → u ⊆ x
10 velpw ⊢ u ∈ 𝒫 x ↔ u ⊆ x
11 9 10 sylibr ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → u ∈ 𝒫 x
12 8 11 elind ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x
13 simprr3 ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x ∧ u ∈ J ∧ u ⊆ x ∧ y ∈ u ∧ J ↾ 𝑡 u ∈ A → J ↾ 𝑡 u ∈ A
14 2 12 13 reximssdv ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x → ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
15 14 3expb ⊢ J ∈ Locally A ∧ x ∈ J ∧ y ∈ x → ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
16 15 ralrimivva ⊢ J ∈ Locally A → ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
17 isnlly ⊢ J ∈ N-Locally A ↔ J ∈ Top ∧ ∀ x ∈ J ∀ y ∈ x ∃ u ∈ nei ⁡ J ⁡ y ∩ 𝒫 x J ↾ 𝑡 u ∈ A
18 1 16 17 sylanbrc ⊢ J ∈ Locally A → J ∈ N-Locally A