Metamath Proof Explorer


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 )