Metamath Proof Explorer

Theorem infxrmnf

Description: The infinimum of a set of extended reals containing minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018) (Revised by AV, 28-Sep-2020)

Ref Expression
Assertion infxrmnf 
|- ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) = -oo )

Proof

Step Hyp Ref Expression
1 infxrlb 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) <_ -oo )
2 infxrcl 
 |-  ( A C_ RR* -> inf ( A , RR* , < ) e. RR* )
3 2 adantr 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) e. RR* )
4 xlemnf 
 |-  ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) <_ -oo <-> inf ( A , RR* , < ) = -oo ) )
5 3 4 syl 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> ( inf ( A , RR* , < ) <_ -oo <-> inf ( A , RR* , < ) = -oo ) )
6 1 5 mpbid 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) = -oo )