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
Assertion iscms M CMetSp M MetSp D CMet X

Proof

Step Hyp Ref Expression
1 iscms.1 X = Base M
2 iscms.2 D = dist M X × X
3 fvexd w = M Base w 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 syl6eqr 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 × b = X × X
11 5 10 reseq12d w = M b = Base w dist w b × b = dist M X × X
12 11 2 syl6eqr w = M b = Base w dist w b × 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 × b CMet b D CMet X
15 3 14 sbcied w = M [˙Base w / b]˙ dist w b × b CMet b D CMet X
16 df-cms CMetSp = w MetSp | [˙Base w / b]˙ dist w b × b CMet b
17 15 16 elrab2 M CMetSp M MetSp D CMet X