Metamath Proof Explorer

Theorem supxrltinfxr

Description: The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion supxrltinfxr 
|- sup ( (/) , RR* , < ) < inf ( (/) , RR* , < )

Proof

Step Hyp Ref Expression
1 mnfltpnf 
 |-  -oo < +oo
2 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
3 xrinf0 
 |-  inf ( (/) , RR* , < ) = +oo
4 1 2 3 3brtr4i 
 |-  sup ( (/) , RR* , < ) < inf ( (/) , RR* , < )