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 ∈ ∞Met ⁡ X → J ∈ Reg

Proof

Step Hyp Ref Expression
1 metnrm.j ⊢ J = MetOpen ⁡ D
2 1 metnrm ⊢ D ∈ ∞Met ⁡ X → J ∈ Nrm
3 1 methaus ⊢ D ∈ ∞Met ⁡ X → J ∈ Haus
4 haust1 ⊢ J ∈ Haus → J ∈ Fre
5 3 4 syl ⊢ D ∈ ∞Met ⁡ X → J ∈ Fre
6 nrmreg ⊢ J ∈ Nrm ∧ J ∈ Fre → J ∈ Reg
7 2 5 6 syl2anc ⊢ D ∈ ∞Met ⁡ X → J ∈ Reg