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 ⊢ B ⊆ ℝ ∧ B ∈ Fin ∧ A ∈ B → sup B ℝ < ≤ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ B ⊆ ℝ ∧ B ∈ Fin ∧ A ∈ B → B ⊆ ℝ
2 fiminre2 ⊢ B ⊆ ℝ ∧ B ∈ Fin → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y
3 2 3adant3 ⊢ B ⊆ ℝ ∧ B ∈ Fin ∧ A ∈ B → ∃ x ∈ ℝ ∀ y ∈ B x ≤ y
4 simp3 ⊢ B ⊆ ℝ ∧ B ∈ Fin ∧ A ∈ B → A ∈ B
5 infrelb ⊢ B ⊆ ℝ ∧ ∃ x ∈ ℝ ∀ y ∈ B x ≤ y ∧ A ∈ B → sup B ℝ < ≤ A
6 1 3 4 5 syl3anc ⊢ B ⊆ ℝ ∧ B ∈ Fin ∧ A ∈ B → sup B ℝ < ≤ A