Metamath Proof Explorer

Theorem hausnlly

Description: A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion hausnlly ⊢ J ∈ N-Locally 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 2 restnlly ⊢ ⊤ → N-Locally Haus = Locally Haus
4 3 mptru ⊢ N-Locally Haus = Locally Haus
5 4 eleq2i ⊢ J ∈ N-Locally Haus ↔ J ∈ Locally Haus