Theorem metreg

Description: A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016)

	Ref	Expression
Hypothesis	metnrm.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
Assertion	metreg	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Reg}$$

Proof

Step	Hyp	Ref	Expression
1		metnrm.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
2	1	metnrm	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Nrm}$$
3	1	methaus	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Haus}$$
4		haust1	$$⊢J\in \mathrm{Haus}\to J\in \mathrm{Fre}$$
5	3 4	syl	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Fre}$$
6		nrmreg	$$⊢\left(J\in \mathrm{Nrm}\wedge J\in \mathrm{Fre}\right)\to J\in \mathrm{Reg}$$
7	2 5 6	syl2anc	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{Reg}$$