Theorem llytop

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

	Ref	Expression
Assertion	llytop	⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		islly	⊢ ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) )
2	1	simplbi	⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top )