This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem haustop

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

Ref Expression
Assertion haustop ⊢ J ∈ Haus → J ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 ishaus ⊢ J ∈ Haus ↔ J ∈ Top ∧ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J x ≠ y → ∃ n ∈ J ∃ m ∈ J x ∈ n ∧ y ∈ m ∧ n ∩ m = ∅
3 2 simplbi ⊢ J ∈ Haus → J ∈ Top