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	⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) = -∞ )

Proof

Step	Hyp	Ref	Expression
1		infxrlb	⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ≤ -∞ )
2		infxrcl	⊢ ( 𝐴 ⊆ ℝ* → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
3	2	adantr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) ∈ ℝ* )
4		xlemnf	⊢ ( inf ( 𝐴 , ℝ* , < ) ∈ ℝ* → ( inf ( 𝐴 , ℝ* , < ) ≤ -∞ ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
5	3 4	syl	⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → ( inf ( 𝐴 , ℝ* , < ) ≤ -∞ ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
6	1 5	mpbid	⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → inf ( 𝐴 , ℝ* , < ) = -∞ )