This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ℝ )