Metamath Proof Explorer

Theorem lerel

Description: "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion lerel 
|- Rel <_

Proof

Step Hyp Ref Expression
1 lerelxr 
 |-  <_ C_ ( RR* X. RR* )
2 relxp 
 |-  Rel ( RR* X. RR* )
3 relss 
 |-  ( <_ C_ ( RR* X. RR* ) -> ( Rel ( RR* X. RR* ) -> Rel <_ ) )
4 1 2 3 mp2 
 |-  Rel <_