Metamath Proof Explorer

Theorem xrgtso

Description: 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion xrgtso 
|- `' < Or RR*

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 cnvso 
 |-  ( < Or RR* <-> `' < Or RR* )
3 1 2 mpbi 
 |-  `' < Or RR*