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	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( CMet ‘ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2	1	recld2	⊢ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) )
3		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
4	3	cncmet	⊢ ( abs ∘ − ) ∈ ( CMet ‘ ℂ )
5	1	cnfldtopn	⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
6	5	cmetss	⊢ ( ( abs ∘ − ) ∈ ( CMet ‘ ℂ ) → ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( CMet ‘ ℝ ) ↔ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) )
7	4 6	ax-mp	⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( CMet ‘ ℝ ) ↔ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
8	2 7	mpbir	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( CMet ‘ ℝ )