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