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	|- ( ph -> B C_ RR )
	supfirege.2	|- ( ph -> B e. Fin )
	supfirege.3	|- ( ph -> C e. B )
	supfirege.4	|- ( ph -> S = sup ( B , RR , < ) )
Assertion	supfirege	|- ( ph -> C <_ S )

Proof

Step	Hyp	Ref	Expression
1		supfirege.1	|- ( ph -> B C_ RR )
2		supfirege.2	|- ( ph -> B e. Fin )
3		supfirege.3	|- ( ph -> C e. B )
4		supfirege.4	|- ( ph -> S = sup ( B , RR , < ) )
5		ltso	|- < Or RR
6	5	a1i	|- ( ph -> < Or RR )
7	6 1 2 3 4	supgtoreq	|- ( ph -> ( C < S \/ C = S ) )
8	1 3	sseldd	|- ( ph -> C e. RR )
9	3	ne0d	|- ( ph -> B =/= (/) )
10		fisupcl	|- ( ( < Or RR /\ ( B e. Fin /\ B =/= (/) /\ B C_ RR ) ) -> sup ( B , RR , < ) e. B )
11	6 2 9 1 10	syl13anc	|- ( ph -> sup ( B , RR , < ) e. B )
12	4 11	eqeltrd	|- ( ph -> S e. B )
13	1 12	sseldd	|- ( ph -> S e. RR )
14	8 13	leloed	|- ( ph -> ( C <_ S <-> ( C < S \/ C = S ) ) )
15	7 14	mpbird	|- ( ph -> C <_ S )