This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ⊆ ℝ * → ∀ x ∈ ℝ ∃ y ∈ A y ≤ x ↔ inf A ℝ * < = −∞

Proof

Step Hyp Ref Expression
1 unb2ltle ⊢ A ⊆ ℝ * → ∀ w ∈ ℝ ∃ y ∈ A y < w ↔ ∀ x ∈ ℝ ∃ y ∈ A y ≤ x
2 infxrunb2 ⊢ A ⊆ ℝ * → ∀ w ∈ ℝ ∃ y ∈ A y < w ↔ inf A ℝ * < = −∞
3 1 2 bitr3d ⊢ A ⊆ ℝ * → ∀ x ∈ ℝ ∃ y ∈ A y ≤ x ↔ inf A ℝ * < = −∞