Theorem cmetmet

Description: A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006) (Revised by Mario Carneiro, 29-Jan-2014)

	Ref	Expression
Assertion	cmetmet	$$⊢D\in \mathrm{CMet}\left(X\right)\to D\in \mathrm{Met}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{MetOpen}\left(D\right)=\mathrm{MetOpen}\left(D\right)$$
2	1	iscmet	$$⊢D\in \mathrm{CMet}\left(X\right)\leftrightarrow \left(D\in \mathrm{Met}\left(X\right)\wedge \forall f\in \mathrm{CauFil}\left(D\right)\mathrm{MetOpen}\left(D\right)\mathrm{fLim}f\ne \varnothing \right)$$
3	2	simplbi	$$⊢D\in \mathrm{CMet}\left(X\right)\to D\in \mathrm{Met}\left(X\right)$$