Metamath Proof Explorer

Theorem retos

Description: The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion retos 
|- RRfld e. Toset

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 idref 
 |-  ( ( _I |` RR ) C_ <_ <-> A. x e. RR x <_ x )
3 leid 
 |-  ( x e. RR -> x <_ x )
4 2 3 mprgbir 
 |-  ( _I |` RR ) C_ <_
5 df-refld 
 |-  RRfld = ( CCfld |`s RR )
6 5 ovexi 
 |-  RRfld e. _V
7 rebase 
 |-  RR = ( Base ` RRfld )
8 rele2 
 |-  <_ = ( le ` RRfld )
9 relt 
 |-  < = ( lt ` RRfld )
10 7 8 9 tosso 
 |-  ( RRfld e. _V -> ( RRfld e. Toset <-> ( < Or RR /\ ( _I |` RR ) C_ <_ ) ) )
11 6 10 ax-mp 
 |-  ( RRfld e. Toset <-> ( < Or RR /\ ( _I |` RR ) C_ <_ ) )
12 1 4 11 mpbir2an 
 |-  RRfld e. Toset