Metamath Proof Explorer


Theorem infrefilb

Description: The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion infrefilb ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → 𝐵 ⊆ ℝ )
2 fiminre2 ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑥𝑦 )
3 2 3adant3 ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑥𝑦 )
4 simp3 ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → 𝐴𝐵 )
5 infrelb ( ( 𝐵 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐵 𝑥𝑦𝐴𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )
6 1 3 4 5 syl3anc ( ( 𝐵 ⊆ ℝ ∧ 𝐵 ∈ Fin ∧ 𝐴𝐵 ) → inf ( 𝐵 , ℝ , < ) ≤ 𝐴 )