Description: If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005) (Revised by AV, 4-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | lbinfcl | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lbinf | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → inf ( 𝑆 , ℝ , < ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ) | |
2 | lbcl | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ∈ 𝑆 ) | |
3 | 1 2 | eqeltrd | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) |