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 ⊢ J ∈ Nrm ∧ J ∈ Fre → J ∈ Reg

Proof

Step Hyp Ref Expression
1 t1r0 ⊢ J ∈ Fre → KQ ⁡ J ∈ Fre
2 nrmr0reg ⊢ J ∈ Nrm ∧ KQ ⁡ J ∈ Fre → J ∈ Reg
3 1 2 sylan2 ⊢ J ∈ Nrm ∧ J ∈ Fre → J ∈ Reg