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 
|- ( 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 )