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

Metamath Proof Explorer

Theorem reghaus

Description: A regular T_0 space is Hausdorff. In other words, a T_3 space is T_2 . A regular Hausdorff or T_0 space is also known as a T_3 space. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion reghaus 
|- ( J e. Reg -> ( J e. Haus <-> J e. Kol2 ) )

Proof

Step Hyp Ref Expression
1 haust1 
 |-  ( J e. Haus -> J e. Fre )
2 t1t0 
 |-  ( J e. Fre -> J e. Kol2 )
3 1 2 syl 
 |-  ( J e. Haus -> J e. Kol2 )
4 regr1 
 |-  ( J e. Reg -> ( KQ ` J ) e. Haus )
5 4 anim2i 
 |-  ( ( J e. Kol2 /\ J e. Reg ) -> ( J e. Kol2 /\ ( KQ ` J ) e. Haus ) )
6 ishaus3 
 |-  ( J e. Haus <-> ( J e. Kol2 /\ ( KQ ` J ) e. Haus ) )
7 5 6 sylibr 
 |-  ( ( J e. Kol2 /\ J e. Reg ) -> J e. Haus )
8 7 expcom 
 |-  ( J e. Reg -> ( J e. Kol2 -> J e. Haus ) )
9 3 8 impbid2 
 |-  ( J e. Reg -> ( J e. Haus <-> J e. Kol2 ) )