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 e. ( CMet ` X ) -> D e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
2 1 iscmet 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( ( MetOpen ` D ) fLim f ) =/= (/) ) )
3 2 simplbi 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )