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 * −∞ A inf A * < = −∞

Proof

Step Hyp Ref Expression
1 infxrlb A * −∞ A inf A * < −∞
2 infxrcl A * inf A * < *
3 2 adantr A * −∞ A inf A * < *
4 xlemnf inf A * < * inf A * < −∞ inf A * < = −∞
5 3 4 syl A * −∞ A inf A * < −∞ inf A * < = −∞
6 1 5 mpbid A * −∞ A inf A * < = −∞