Metamath Proof Explorer

Theorem ltrel

Description: "Less than" is a relation. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion ltrel 
|- Rel <

Proof

Step Hyp Ref Expression
1 ltrelxr 
 |-  < 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 <