This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑆 , ℝ , < ) = ( ℩ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) )