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)\upharpoonright }_{\left(X\times X\right)}$$
Assertion	iscms	$$⊢M\in \mathrm{CMetSp}\leftrightarrow \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)\upharpoonright }_{\left(X\times 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	eqtr4di	$$⊢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\times b=X\times X$$
11	5 10	reseq12d	$$⊢\left(w=M\wedge b={\mathrm{Base}}_w\right)\to {\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}={\mathrm{dist}\left(M\right)\upharpoonright }_{\left(X\times X\right)}$$
12	11 2	eqtr4di	$$⊢\left(w=M\wedge b={\mathrm{Base}}_w\right)\to {\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times 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)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\leftrightarrow D\in \mathrm{CMet}\left(X\right)\right)$$
15	3 14	sbcied	$$⊢w=M\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\leftrightarrow D\in \mathrm{CMet}\left(X\right)\right)$$
16		df-cms	$$⊢\mathrm{CMetSp}=\left\{w\in \mathrm{MetSp}|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}{\mathrm{dist}\left(w\right)\upharpoonright }_{\left(b\times b\right)}\in \mathrm{CMet}\left(b\right)\right\}$$
17	15 16	elrab2	$$⊢M\in \mathrm{CMetSp}\leftrightarrow \left(M\in \mathrm{MetSp}\wedge D\in \mathrm{CMet}\left(X\right)\right)$$