Theorem recmet

Description: The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	recmet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{CMet}\left(ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	recld2	$$⊢ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
3		eqid	$$⊢\mathrm{abs}\circ -=\mathrm{abs}\circ -$$
4	3	cncmet	$$⊢\mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)$$
5	1	cnfldtopn	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)$$
6	5	cmetss	$$⊢\mathrm{abs}\circ -\in \mathrm{CMet}\left(ℂ\right)\to \left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{CMet}\left(ℝ\right)\leftrightarrow ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$$
7	4 6	ax-mp	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{CMet}\left(ℝ\right)\leftrightarrow ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
8	2 7	mpbir	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{CMet}\left(ℝ\right)$$