Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fimaxre3 Structured version   Unicode version

Theorem fimaxre3 10493
 Description: A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014.)
Assertion
Ref Expression
fimaxre3
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem fimaxre3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.29 2976 . . . . . 6
2 eleq1 2513 . . . . . . . 8
32biimparc 487 . . . . . . 7
43rexlimivw 2930 . . . . . 6
51, 4syl 16 . . . . 5
65ex 434 . . . 4
76abssdv 3556 . . 3
8 abrexfi 7818 . . 3
9 fimaxre2 10492 . . 3
107, 8, 9syl2anr 478 . 2
11 r19.23v 2921 . . . . . . 7
1211albii 1625 . . . . . 6
13 ralcom4 3112 . . . . . 6
14 eqeq1 2445 . . . . . . . 8
1514rexbidv 2952 . . . . . . 7
1615ralab 3244 . . . . . 6
1712, 13, 163bitr4i 277 . . . . 5
18 nfv 1692 . . . . . . . 8
19 breq1 4436 . . . . . . . 8
2018, 19ceqsalg 3118 . . . . . . 7
2120ralimi 2834 . . . . . 6
22 ralbi 2972 . . . . . 6
2321, 22syl 16 . . . . 5
2417, 23syl5bbr 259 . . . 4
2524rexbidv 2952 . . 3