Metamath Proof Explorer


Theorem lbinfcl

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 ( 𝑆 , ℝ , < ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lbinf ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → inf ( 𝑆 , ℝ , < ) = ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) )
2 lbcl ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 )
3 1 2 eqeltrd ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 )