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

Metamath Proof Explorer

Theorem supfirege

Description: The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019)

Ref Expression
Hypotheses supfirege.1 ⊢ φ → B ⊆ ℝ
supfirege.2 ⊢ φ → B ∈ Fin
supfirege.3 ⊢ φ → C ∈ B
supfirege.4 ⊢ φ → S = sup B ℝ <
Assertion supfirege ⊢ φ → C ≤ S

Proof

Step Hyp Ref Expression
1 supfirege.1 ⊢ φ → B ⊆ ℝ
2 supfirege.2 ⊢ φ → B ∈ Fin
3 supfirege.3 ⊢ φ → C ∈ B
4 supfirege.4 ⊢ φ → S = sup B ℝ <
5 ltso ⊢ < Or ℝ
6 5 a1i ⊢ φ → < Or ℝ
7 6 1 2 3 4 supgtoreq ⊢ φ → C < S ∨ C = S
8 1 3 sseldd ⊢ φ → C ∈ ℝ
9 3 ne0d ⊢ φ → B ≠ ∅
10 fisupcl ⊢ < Or ℝ ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ ℝ → sup B ℝ < ∈ B
11 6 2 9 1 10 syl13anc ⊢ φ → sup B ℝ < ∈ B
12 4 11 eqeltrd ⊢ φ → S ∈ B
13 1 12 sseldd ⊢ φ → S ∈ ℝ
14 8 13 leloed ⊢ φ → C ≤ S ↔ C < S ∨ C = S
15 7 14 mpbird ⊢ φ → C ≤ S