Description: The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | infxrglb | ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( inf ( 𝐴 , ℝ* , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrltso | ⊢ < Or ℝ* | |
2 | 1 | a1i | ⊢ ( 𝐴 ⊆ ℝ* → < Or ℝ* ) |
3 | xrinfmss | ⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑧 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑥 < 𝑦 ) ) ) | |
4 | id | ⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ⊆ ℝ* ) | |
5 | 2 3 4 | infglbb | ⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( inf ( 𝐴 , ℝ* , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) ) |