Theorem metreg

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

	Ref	Expression
Hypothesis	metnrm.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	metreg	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Reg )

Proof

Step	Hyp	Ref	Expression
1		metnrm.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2	1	metnrm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Nrm )
3	1	methaus	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
4		haust1	⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Fre )
5	3 4	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Fre )
6		nrmreg	⊢ ( ( 𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre ) → 𝐽 ∈ Reg )
7	2 5 6	syl2anc	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Reg )