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 )