Metamath Proof Explorer

Theorem recusp

Description: The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion recusp 
|- RRfld e. CUnifSp

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 ne0ii 
 |-  RR =/= (/)
3 recms 
 |-  RRfld e. CMetSp
4 reust 
 |-  ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )
5 rebase 
 |-  RR = ( Base ` RRfld )
6 eqid 
 |-  ( ( dist ` RRfld ) |` ( RR X. RR ) ) = ( ( dist ` RRfld ) |` ( RR X. RR ) )
7 eqid 
 |-  ( UnifSt ` RRfld ) = ( UnifSt ` RRfld )
8 5 6 7 cmetcusp1 
 |-  ( ( RR =/= (/) /\ RRfld e. CMetSp /\ ( UnifSt ` RRfld ) = ( metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) ) ) -> RRfld e. CUnifSp )
9 2 3 4 8 mp3an 
 |-  RRfld e. CUnifSp