# 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}={\mathrm{Base}}_{{M}}$
iscms.2 ${⊢}{D}={\mathrm{dist}\left({M}\right)↾}_{\left({X}×{X}\right)}$
Assertion iscms ${⊢}{M}\in \mathrm{CMetSp}↔\left({M}\in \mathrm{MetSp}\wedge {D}\in \mathrm{CMet}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 iscms.1 ${⊢}{X}={\mathrm{Base}}_{{M}}$
2 iscms.2 ${⊢}{D}={\mathrm{dist}\left({M}\right)↾}_{\left({X}×{X}\right)}$
3 fvexd ${⊢}{w}={M}\to {\mathrm{Base}}_{{w}}\in \mathrm{V}$
4 fveq2 ${⊢}{w}={M}\to \mathrm{dist}\left({w}\right)=\mathrm{dist}\left({M}\right)$
5 4 adantr ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to \mathrm{dist}\left({w}\right)=\mathrm{dist}\left({M}\right)$
6 id ${⊢}{b}={\mathrm{Base}}_{{w}}\to {b}={\mathrm{Base}}_{{w}}$
7 fveq2 ${⊢}{w}={M}\to {\mathrm{Base}}_{{w}}={\mathrm{Base}}_{{M}}$
8 7 1 syl6eqr ${⊢}{w}={M}\to {\mathrm{Base}}_{{w}}={X}$
9 6 8 sylan9eqr ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to {b}={X}$
10 9 sqxpeqd ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to {b}×{b}={X}×{X}$
11 5 10 reseq12d ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to {\mathrm{dist}\left({w}\right)↾}_{\left({b}×{b}\right)}={\mathrm{dist}\left({M}\right)↾}_{\left({X}×{X}\right)}$
12 11 2 syl6eqr ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to {\mathrm{dist}\left({w}\right)↾}_{\left({b}×{b}\right)}={D}$
13 9 fveq2d ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to \mathrm{CMet}\left({b}\right)=\mathrm{CMet}\left({X}\right)$
14 12 13 eleq12d ${⊢}\left({w}={M}\wedge {b}={\mathrm{Base}}_{{w}}\right)\to \left({\mathrm{dist}\left({w}\right)↾}_{\left({b}×{b}\right)}\in \mathrm{CMet}\left({b}\right)↔{D}\in \mathrm{CMet}\left({X}\right)\right)$
15 3 14 sbcied
16 df-cms
17 15 16 elrab2 ${⊢}{M}\in \mathrm{CMetSp}↔\left({M}\in \mathrm{MetSp}\wedge {D}\in \mathrm{CMet}\left({X}\right)\right)$