Metamath Proof Explorer

Theorem hauslly

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

Ref Expression
Assertion hauslly ⊢ J ∈ Haus → J ∈ Locally Haus

Proof

Step Hyp Ref Expression
1 resthaus ⊢ j ∈ Haus ∧ x ∈ j → j ↾ 𝑡 x ∈ Haus
2 1 adantl ⊢ ⊤ ∧ j ∈ Haus ∧ x ∈ j → j ↾ 𝑡 x ∈ Haus
3 haustop ⊢ j ∈ Haus → j ∈ Top
4 3 ssriv ⊢ Haus ⊆ Top
5 4 a1i ⊢ ⊤ → Haus ⊆ Top
6 2 5 restlly ⊢ ⊤ → Haus ⊆ Locally Haus
7 6 mptru ⊢ Haus ⊆ Locally Haus
8 7 sseli ⊢ J ∈ Haus → J ∈ Locally Haus