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 )