Metamath Proof Explorer

Theorem xrltso

Description: 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005)

Ref Expression
Assertion xrltso 
|- < Or RR*

Proof

Step Hyp Ref Expression
1 xrlttri 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x < y <-> -. ( x = y \/ y < x ) ) )
2 xrlttr 
 |-  ( ( x e. RR* /\ y e. RR* /\ z e. RR* ) -> ( ( x < y /\ y < z ) -> x < z ) )
3 1 2 isso2i 
 |-  < Or RR*