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	$$⊢\phi \to B\subseteq ℝ$$
	supfirege.2	$$⊢\phi \to B\in \mathrm{Fin}$$
	supfirege.3	$$⊢\phi \to C\in B$$
	supfirege.4	$$⊢\phi \to S=sup\left(B,ℝ,<\right)$$
Assertion	supfirege	$$⊢\phi \to C\le S$$

Proof

Step	Hyp	Ref	Expression
1		supfirege.1	$$⊢\phi \to B\subseteq ℝ$$
2		supfirege.2	$$⊢\phi \to B\in \mathrm{Fin}$$
3		supfirege.3	$$⊢\phi \to C\in B$$
4		supfirege.4	$$⊢\phi \to S=sup\left(B,ℝ,<\right)$$
5		ltso	$$⊢<\mathrm{Or}ℝ$$
6	5	a1i	$$⊢\phi \to <\mathrm{Or}ℝ$$
7	6 1 2 3 4	supgtoreq	$$⊢\phi \to \left(C<S\vee C=S\right)$$
8	1 3	sseldd	$$⊢\phi \to C\in ℝ$$
9	3	ne0d	$$⊢\phi \to B\ne \varnothing$$
10		fisupcl	$$⊢\left(<\mathrm{Or}ℝ\wedge \left(B\in \mathrm{Fin}\wedge B\ne \varnothing \wedge B\subseteq ℝ\right)\right)\to sup\left(B,ℝ,<\right)\in B$$
11	6 2 9 1 10	syl13anc	$$⊢\phi \to sup\left(B,ℝ,<\right)\in B$$
12	4 11	eqeltrd	$$⊢\phi \to S\in B$$
13	1 12	sseldd	$$⊢\phi \to S\in ℝ$$
14	8 13	leloed	$$⊢\phi \to \left(C\le S\leftrightarrow \left(C<S\vee C=S\right)\right)$$
15	7 14	mpbird	$$⊢\phi \to C\le S$$