Metamath Proof Explorer


Theorem haustop

Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007)

Ref Expression
Assertion haustop ( 𝐽 ∈ Haus → 𝐽 ∈ Top )

Proof

Step Hyp Ref Expression
1 eqid 𝐽 = 𝐽
2 1 ishaus ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 𝐽𝑦 𝐽 ( 𝑥𝑦 → ∃ 𝑛𝐽𝑚𝐽 ( 𝑥𝑛𝑦𝑚 ∧ ( 𝑛𝑚 ) = ∅ ) ) ) )
3 2 simplbi ( 𝐽 ∈ Haus → 𝐽 ∈ Top )