Metamath Proof Explorer

Theorem xrinfm

Description: The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018) (Revised by AV, 28-Sep-2020)

Ref Expression
Assertion xrinfm 
|- inf ( RR* , RR* , < ) = -oo

Proof

Step Hyp Ref Expression
1 ssid 
 |-  RR* C_ RR*
2 mnfxr 
 |-  -oo e. RR*
3 infxrmnf 
 |-  ( ( RR* C_ RR* /\ -oo e. RR* ) -> inf ( RR* , RR* , < ) = -oo )
4 1 2 3 mp2an 
 |-  inf ( RR* , RR* , < ) = -oo