Theorem nllytop

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

	Ref	Expression
Assertion	nllytop	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		isnlly	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) )
2	1	simplbi	⊢ ( 𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top )