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∩𝒫xJ↾𝑡u∈A
2 1 simplbi ⊢J∈N-Locally A → J∈Top