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 \in Reg \to (J \in Haus \leftrightarrow J \in Kol2)$

Proof

Step	Hyp	Ref	Expression
1		haust1	$⊢ J \in Haus \to J \in Fre$
2		t1t0	$⊢ J \in Fre \to J \in Kol2$
3	1 2	syl	$⊢ J \in Haus \to J \in Kol2$
4		regr1	$⊢ J \in Reg \to KQ (J) \in Haus$
5	4	anim2i	$⊢ (J \in Kol2 \land J \in Reg) \to (J \in Kol2 \land KQ (J) \in Haus)$
6		ishaus3	$⊢ J \in Haus \leftrightarrow (J \in Kol2 \land KQ (J) \in Haus)$
7	5 6	sylibr	$⊢ (J \in Kol2 \land J \in Reg) \to J \in Haus$
8	7	expcom	$⊢ J \in Reg \to (J \in Kol2 \to J \in Haus)$
9	3 8	impbid2	$⊢ J \in Reg \to (J \in Haus \leftrightarrow J \in Kol2)$

Metamath Proof Explorer

Theorem reghaus

Proof