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	⊢ ( 𝐽 ∈ Reg → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2 ) )

Proof

Step	Hyp	Ref	Expression
1		haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )
2		t1t0	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )
3	1 2	syl	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Kol2 )
4		regr1	⊢ ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Haus )
5	4	anim2i	⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝐽 ∈ Reg ) → ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ Haus ) )
6		ishaus3	⊢ ( 𝐽 ∈ Haus ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ Haus ) )
7	5 6	sylibr	⊢ ( ( 𝐽 ∈ Kol2 ∧ 𝐽 ∈ Reg ) → 𝐽 ∈ Haus )
8	7	expcom	⊢ ( 𝐽 ∈ Reg → ( 𝐽 ∈ Kol2 → 𝐽 ∈ Haus ) )
9	3 8	impbid2	⊢ ( 𝐽 ∈ Reg → ( 𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2 ) )