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 ) )