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 ( 𝜑𝐶𝑆 )