Theorem metreg

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

	Ref	Expression
Hypothesis	metnrm.j	|- J = ( MetOpen ` D )
Assertion	metreg	|- ( D e. ( *Met ` X ) -> J e. Reg )

Proof

Step	Hyp	Ref	Expression
1		metnrm.j	|- J = ( MetOpen ` D )
2	1	metnrm	|- ( D e. ( *Met ` X ) -> J e. Nrm )
3	1	methaus	|- ( D e. ( *Met ` X ) -> J e. Haus )
4		haust1	|- ( J e. Haus -> J e. Fre )
5	3 4	syl	|- ( D e. ( *Met ` X ) -> J e. Fre )
6		nrmreg	|- ( ( J e. Nrm /\ J e. Fre ) -> J e. Reg )
7	2 5 6	syl2anc	|- ( D e. ( *Met ` X ) -> J e. Reg )