Metamath Proof Explorer

Theorem nllytop

Description: A locally A space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion nllytop ⊢ J ∈ N-Locally A → J ∈ Top

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 simplbi ⊢ J ∈ N-Locally A → J ∈ Top