Metamath Proof Explorer


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 )