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 )