Metamath Proof Explorer

Theorem xrslt

Description: The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Assertion xrslt 
|- < = ( lt ` RR*s )

Proof

Step Hyp Ref Expression
1 dflt2 
 |-  < = ( <_ \ _I )
2 xrsex 
 |-  RR*s e. _V
3 xrsle 
 |-  <_ = ( le ` RR*s )
4 eqid 
 |-  ( lt ` RR*s ) = ( lt ` RR*s )
5 3 4 pltfval 
 |-  ( RR*s e. _V -> ( lt ` RR*s ) = ( <_ \ _I ) )
6 2 5 ax-mp 
 |-  ( lt ` RR*s ) = ( <_ \ _I )
7 1 6 eqtr4i 
 |-  < = ( lt ` RR*s )