Description: If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lbinfle | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lbinf | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → inf ( 𝑆 , ℝ , < ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ) | |
| 2 | 1 | 3adant3 | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ) |
| 3 | lble | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ≤ 𝐴 ) | |
| 4 | 2 3 | eqbrtrd | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 ) |