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 o. - ) |` ( RR X. RR ) ) e. ( CMet ` RR )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
3 eqid 
 |-  ( abs o. - ) = ( abs o. - )
4 3 cncmet 
 |-  ( abs o. - ) e. ( CMet ` CC )
5 1 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
6 5 cmetss 
 |-  ( ( abs o. - ) e. ( CMet ` CC ) -> ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( CMet ` RR ) <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) ) )
7 4 6 ax-mp 
 |-  ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( CMet ` RR ) <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) )
8 2 7 mpbir 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( CMet ` RR )