Theorem infxrunb3

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	infxrunb3	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )

Proof

Step	Hyp	Ref	Expression
1		unb2ltle	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
2		infxrunb2	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )
3	1 2	bitr3d	⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ↔ inf ( 𝐴 , ℝ* , < ) = -∞ ) )