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

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 )