Metamath Proof Explorer

Theorem fimaxre

Description: A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Steven Nguyen, 3-Jun-2023)

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

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 soss 
 |-  ( A C_ RR -> ( < Or RR -> < Or A ) )
3 1 2 mpi 
 |-  ( A C_ RR -> < Or A )
4 fimaxg 
 |-  ( ( < Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> y < x ) )
5 3 4 syl3an1 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A ( x =/= y -> y < x ) )
6 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
7 6 adantrl 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> y e. RR )
8 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
9 8 adantrr 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> x e. RR )
10 7 9 leloed 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
11 orcom 
 |-  ( ( x = y \/ y < x ) <-> ( y < x \/ x = y ) )
12 equcom 
 |-  ( x = y <-> y = x )
13 12 orbi2i 
 |-  ( ( y < x \/ x = y ) <-> ( y < x \/ y = x ) )
14 11 13 bitri 
 |-  ( ( x = y \/ y < x ) <-> ( y < x \/ y = x ) )
15 14 a1i 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> ( ( x = y \/ y < x ) <-> ( y < x \/ y = x ) ) )
16 neor 
 |-  ( ( x = y \/ y < x ) <-> ( x =/= y -> y < x ) )
17 16 a1i 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> ( ( x = y \/ y < x ) <-> ( x =/= y -> y < x ) ) )
18 10 15 17 3bitr2d 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> ( y <_ x <-> ( x =/= y -> y < x ) ) )
19 18 biimprd 
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. A ) ) -> ( ( x =/= y -> y < x ) -> y <_ x ) )
20 19 anassrs 
 |-  ( ( ( A C_ RR /\ x e. A ) /\ y e. A ) -> ( ( x =/= y -> y < x ) -> y <_ x ) )
21 20 ralimdva 
 |-  ( ( A C_ RR /\ x e. A ) -> ( A. y e. A ( x =/= y -> y < x ) -> A. y e. A y <_ x ) )
22 21 reximdva 
 |-  ( A C_ RR -> ( E. x e. A A. y e. A ( x =/= y -> y < x ) -> E. x e. A A. y e. A y <_ x ) )
23 22 3ad2ant1 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> ( E. x e. A A. y e. A ( x =/= y -> y < x ) -> E. x e. A A. y e. A y <_ x ) )
24 5 23 mpd 
 |-  ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )