Metamath Proof Explorer

Theorem lerelxr

Description: "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion lerelxr 
|- <_ C_ ( RR* X. RR* )

Proof

Step Hyp Ref Expression
1 df-le 
 |-  <_ = ( ( RR* X. RR* ) \ `' < )
2 difss 
 |-  ( ( RR* X. RR* ) \ `' < ) C_ ( RR* X. RR* )
3 1 2 eqsstri 
 |-  <_ C_ ( RR* X. RR* )