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 ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
supfirege.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
supfirege.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
supfirege.4 ⊢ ( 𝜑 → 𝑆 = sup ( 𝐵 , ℝ , < ) )
Assertion supfirege ( 𝜑 → 𝐶 ≤ 𝑆 )

Proof

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