Metamath Proof Explorer

Theorem iscms

Description: A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses iscms.1 
|- X = ( Base ` M )
iscms.2 
|- D = ( ( dist ` M ) |` ( X X. X ) )
Assertion iscms 
|- ( M e. CMetSp <-> ( M e. MetSp /\ D e. ( CMet ` X ) ) )

Proof

Step Hyp Ref Expression
1 iscms.1 
 |-  X = ( Base ` M )
2 iscms.2 
 |-  D = ( ( dist ` M ) |` ( X X. X ) )
3 fvexd 
 |-  ( w = M -> ( Base ` w ) e. _V )
4 fveq2 
 |-  ( w = M -> ( dist ` w ) = ( dist ` M ) )
5 4 adantr 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( dist ` w ) = ( dist ` M ) )
6 id 
 |-  ( b = ( Base ` w ) -> b = ( Base ` w ) )
7 fveq2 
 |-  ( w = M -> ( Base ` w ) = ( Base ` M ) )
8 7 1 eqtr4di 
 |-  ( w = M -> ( Base ` w ) = X )
9 6 8 sylan9eqr 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> b = X )
10 9 sqxpeqd 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( b X. b ) = ( X X. X ) )
11 5 10 reseq12d 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( ( dist ` w ) |` ( b X. b ) ) = ( ( dist ` M ) |` ( X X. X ) ) )
12 11 2 eqtr4di 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( ( dist ` w ) |` ( b X. b ) ) = D )
13 9 fveq2d 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( CMet ` b ) = ( CMet ` X ) )
14 12 13 eleq12d 
 |-  ( ( w = M /\ b = ( Base ` w ) ) -> ( ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) <-> D e. ( CMet ` X ) ) )
15 3 14 sbcied 
 |-  ( w = M -> ( [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) <-> D e. ( CMet ` X ) ) )
16 df-cms 
 |-  CMetSp = { w e. MetSp | [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) }
17 15 16 elrab2 
 |-  ( M e. CMetSp <-> ( M e. MetSp /\ D e. ( CMet ` X ) ) )