Metamath Proof Explorer

Theorem xrge0le

Description: The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018)

Ref Expression
Assertion xrge0le 
|- <_ = ( le ` ( RR*s |`s ( 0 [,] +oo ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( 0 [,] +oo ) e. _V
2 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
3 xrsle 
 |-  <_ = ( le ` RR*s )
4 2 3 ressle 
 |-  ( ( 0 [,] +oo ) e. _V -> <_ = ( le ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
5 1 4 ax-mp 
 |-  <_ = ( le ` ( RR*s |`s ( 0 [,] +oo ) ) )