Metamath Proof Explorer


Theorem fimaxre3

Description: A nonempty finite set of real numbers has a maximum (image set version). (Contributed by Mario Carneiro, 13-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 r19.29
 |-  ( ( A. y e. A B e. RR /\ E. y e. A z = B ) -> E. y e. A ( B e. RR /\ z = B ) )
2 eleq1
 |-  ( z = B -> ( z e. RR <-> B e. RR ) )
3 2 biimparc
 |-  ( ( B e. RR /\ z = B ) -> z e. RR )
4 3 rexlimivw
 |-  ( E. y e. A ( B e. RR /\ z = B ) -> z e. RR )
5 1 4 syl
 |-  ( ( A. y e. A B e. RR /\ E. y e. A z = B ) -> z e. RR )
6 5 ex
 |-  ( A. y e. A B e. RR -> ( E. y e. A z = B -> z e. RR ) )
7 6 abssdv
 |-  ( A. y e. A B e. RR -> { z | E. y e. A z = B } C_ RR )
8 abrexfi
 |-  ( A e. Fin -> { z | E. y e. A z = B } e. Fin )
9 fimaxre2
 |-  ( ( { z | E. y e. A z = B } C_ RR /\ { z | E. y e. A z = B } e. Fin ) -> E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x )
10 7 8 9 syl2anr
 |-  ( ( A e. Fin /\ A. y e. A B e. RR ) -> E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x )
11 r19.23v
 |-  ( A. y e. A ( w = B -> w <_ x ) <-> ( E. y e. A w = B -> w <_ x ) )
12 11 albii
 |-  ( A. w A. y e. A ( w = B -> w <_ x ) <-> A. w ( E. y e. A w = B -> w <_ x ) )
13 ralcom4
 |-  ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. w A. y e. A ( w = B -> w <_ x ) )
14 eqeq1
 |-  ( z = w -> ( z = B <-> w = B ) )
15 14 rexbidv
 |-  ( z = w -> ( E. y e. A z = B <-> E. y e. A w = B ) )
16 15 ralab
 |-  ( A. w e. { z | E. y e. A z = B } w <_ x <-> A. w ( E. y e. A w = B -> w <_ x ) )
17 12 13 16 3bitr4i
 |-  ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. w e. { z | E. y e. A z = B } w <_ x )
18 nfv
 |-  F/ w B <_ x
19 breq1
 |-  ( w = B -> ( w <_ x <-> B <_ x ) )
20 18 19 ceqsalg
 |-  ( B e. RR -> ( A. w ( w = B -> w <_ x ) <-> B <_ x ) )
21 20 ralimi
 |-  ( A. y e. A B e. RR -> A. y e. A ( A. w ( w = B -> w <_ x ) <-> B <_ x ) )
22 ralbi
 |-  ( A. y e. A ( A. w ( w = B -> w <_ x ) <-> B <_ x ) -> ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. y e. A B <_ x ) )
23 21 22 syl
 |-  ( A. y e. A B e. RR -> ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. y e. A B <_ x ) )
24 17 23 bitr3id
 |-  ( A. y e. A B e. RR -> ( A. w e. { z | E. y e. A z = B } w <_ x <-> A. y e. A B <_ x ) )
25 24 rexbidv
 |-  ( A. y e. A B e. RR -> ( E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x <-> E. x e. RR A. y e. A B <_ x ) )
26 25 adantl
 |-  ( ( A e. Fin /\ A. y e. A B e. RR ) -> ( E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x <-> E. x e. RR A. y e. A B <_ x ) )
27 10 26 mpbid
 |-  ( ( A e. Fin /\ A. y e. A B e. RR ) -> E. x e. RR A. y e. A B <_ x )