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	$$⊢\left(J\in \mathrm{Nrm}\wedge J\in \mathrm{Fre}\right)\to J\in \mathrm{Reg}$$

Proof

Step	Hyp	Ref	Expression
1		t1r0	$$⊢J\in \mathrm{Fre}\to \mathrm{KQ}\left(J\right)\in \mathrm{Fre}$$
2		nrmr0reg	$$⊢\left(J\in \mathrm{Nrm}\wedge \mathrm{KQ}\left(J\right)\in \mathrm{Fre}\right)\to J\in \mathrm{Reg}$$
3	1 2	sylan2	$$⊢\left(J\in \mathrm{Nrm}\wedge J\in \mathrm{Fre}\right)\to J\in \mathrm{Reg}$$