Metamath Proof Explorer

Theorem relt

Description: The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018)

Ref Expression
Assertion relt 
|- < = ( lt ` RRfld )

Proof

Step Hyp Ref Expression
1 dflt2 
 |-  < = ( <_ \ _I )
2 df-refld 
 |-  RRfld = ( CCfld |`s RR )
3 2 ovexi 
 |-  RRfld e. _V
4 rele2 
 |-  <_ = ( le ` RRfld )
5 eqid 
 |-  ( lt ` RRfld ) = ( lt ` RRfld )
6 4 5 pltfval 
 |-  ( RRfld e. _V -> ( lt ` RRfld ) = ( <_ \ _I ) )
7 3 6 ax-mp 
 |-  ( lt ` RRfld ) = ( <_ \ _I )
8 1 7 eqtr4i 
 |-  < = ( lt ` RRfld )