This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fimaxre2

Description: A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011) (Revised by Mario Carneiro, 13-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 rzal 
 |-  ( A = (/) -> A. y e. A y <_ 0 )
3 brralrspcev 
 |-  ( ( 0 e. RR /\ A. y e. A y <_ 0 ) -> E. x e. RR A. y e. A y <_ x )
4 1 2 3 sylancr 
 |-  ( A = (/) -> E. x e. RR A. y e. A y <_ x )
5 4 a1i 
 |-  ( ( A C_ RR /\ A e. Fin ) -> ( A = (/) -> E. x e. RR A. y e. A y <_ x ) )
6 fimaxre 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )
7 6 3expia 
 |-  ( ( A C_ RR /\ A e. Fin ) -> ( A =/= (/) -> E. x e. A A. y e. A y <_ x ) )
8 ssrexv 
 |-  ( A C_ RR -> ( E. x e. A A. y e. A y <_ x -> E. x e. RR A. y e. A y <_ x ) )
9 8 adantr 
 |-  ( ( A C_ RR /\ A e. Fin ) -> ( E. x e. A A. y e. A y <_ x -> E. x e. RR A. y e. A y <_ x ) )
10 7 9 syld 
 |-  ( ( A C_ RR /\ A e. Fin ) -> ( A =/= (/) -> E. x e. RR A. y e. A y <_ x ) )
11 5 10 pm2.61dne 
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x )