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 )