Metamath Proof Explorer


Theorem fiminre2

Description: A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion fiminre2
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )

Proof

Step Hyp Ref Expression
1 0red
 |-  ( A = (/) -> 0 e. RR )
2 rzal
 |-  ( A = (/) -> A. y e. A 0 <_ y )
3 breq1
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
4 3 ralbidv
 |-  ( x = 0 -> ( A. y e. A x <_ y <-> A. y e. A 0 <_ y ) )
5 4 rspcev
 |-  ( ( 0 e. RR /\ A. y e. A 0 <_ y ) -> E. x e. RR A. y e. A x <_ y )
6 1 2 5 syl2anc
 |-  ( A = (/) -> E. x e. RR A. y e. A x <_ y )
7 6 adantl
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A = (/) ) -> E. x e. RR A. y e. A x <_ y )
8 neqne
 |-  ( -. A = (/) -> A =/= (/) )
9 8 adantl
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ -. A = (/) ) -> A =/= (/) )
10 simpll
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A C_ RR )
11 simplr
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A e. Fin )
12 simpr
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A =/= (/) )
13 fiminre
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )
14 10 11 12 13 syl3anc
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y )
15 ssrexv
 |-  ( A C_ RR -> ( E. x e. A A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y ) )
16 10 14 15 sylc
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> E. x e. RR A. y e. A x <_ y )
17 9 16 syldan
 |-  ( ( ( A C_ RR /\ A e. Fin ) /\ -. A = (/) ) -> E. x e. RR A. y e. A x <_ y )
18 7 17 pm2.61dan
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )