Metamath Proof Explorer


Theorem lbcl

Description: If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion lbcl ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 lbreu ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ∃! 𝑥𝑆𝑦𝑆 𝑥𝑦 )
2 riotacl ( ∃! 𝑥𝑆𝑦𝑆 𝑥𝑦 → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 )
3 1 2 syl ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 )