Metamath Proof Explorer

Theorem haustop

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

Ref Expression
Assertion haustop 
|- ( J e. Haus -> J e. Top )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 ishaus 
 |-  ( J e. Haus <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) )
3 2 simplbi 
 |-  ( J e. Haus -> J e. Top )