Description: A locally A space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | llytop | ⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | islly | ⊢ ( 𝐽 ∈ Locally 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( 𝐽 ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑢 ∧ ( 𝐽 ↾t 𝑢 ) ∈ 𝐴 ) ) ) | |
2 | 1 | simplbi | ⊢ ( 𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top ) |