Description: The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | infrglb | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( inf ( 𝐴 , ℝ , < ) < 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltso | ⊢ < Or ℝ | |
| 2 | 1 | a1i | ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → < Or ℝ ) |
| 3 | infm3 | ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) | |
| 4 | simp1 | ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ ) | |
| 5 | 2 3 4 | infglbb | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐵 ∈ ℝ ) → ( inf ( 𝐴 , ℝ , < ) < 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝐵 ) ) |