Metamath Proof Explorer


Theorem lbinf

Description: If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion lbinf ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → inf ( 𝑆 , ℝ , < ) = ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) )

Proof

Step Hyp Ref Expression
1 ltso < Or ℝ
2 1 a1i ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → < Or ℝ )
3 lbcl ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 )
4 ssel ( 𝑆 ⊆ ℝ → ( ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ ℝ ) )
5 4 adantr ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ 𝑆 → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ ℝ ) )
6 3 5 mpd ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ ℝ )
7 6 adantr ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∧ 𝑧𝑆 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∈ ℝ )
8 ssel2 ( ( 𝑆 ⊆ ℝ ∧ 𝑧𝑆 ) → 𝑧 ∈ ℝ )
9 8 adantlr ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∧ 𝑧𝑆 ) → 𝑧 ∈ ℝ )
10 lble ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦𝑧𝑆 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ≤ 𝑧 )
11 10 3expa ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∧ 𝑧𝑆 ) → ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ≤ 𝑧 )
12 7 9 11 lensymd ( ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) ∧ 𝑧𝑆 ) → ¬ 𝑧 < ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) )
13 2 6 3 12 infmin ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑥𝑆𝑦𝑆 𝑥𝑦 ) → inf ( 𝑆 , ℝ , < ) = ( 𝑥𝑆𝑦𝑆 𝑥𝑦 ) )