This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmetmet

Description: A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006) (Revised by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion cmetmet ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
2 1 iscmet ⊢ D ∈ CMet ⁡ X ↔ D ∈ Met ⁡ X ∧ ∀ f ∈ CauFil ⁡ D MetOpen ⁡ D fLim f ≠ ∅
3 2 simplbi ⊢ D ∈ CMet ⁡ X → D ∈ Met ⁡ X