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 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 × b = X × X
11 5 10 reseq12d ⊢ w = M ∧ b = Base w → dist ⁡ w ↾ b × b = dist ⁡ M ↾ X × X
12 11 2 eqtr4di ⊢ 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