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

Metamath Proof Explorer

Theorem nrmreg

Description: A normal T_1 space is regular Hausdorff. In other words, a T_4 space is T_3 . One can get away with slightly weaker assumptions; see nrmr0reg . (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	nrmreg	⊢ ( ( 𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre ) → 𝐽 ∈ Reg )

Proof

Step	Hyp	Ref	Expression
1		t1r0	⊢ ( 𝐽 ∈ Fre → ( KQ ‘ 𝐽 ) ∈ Fre )
2		nrmr0reg	⊢ ( ( 𝐽 ∈ Nrm ∧ ( KQ ‘ 𝐽 ) ∈ Fre ) → 𝐽 ∈ Reg )
3	1 2	sylan2	⊢ ( ( 𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre ) → 𝐽 ∈ Reg )