Metamath Proof Explorer

Theorem erdsze

Description: The Erdős-Szekeres theorem. For any injective sequence F on the reals of length at least ( R - 1 ) x. ( S - 1 ) + 1 , there is either a subsequence of length at least R on which F is increasing (i.e. a < , < order isomorphism) or a subsequence of length at least S on which F is decreasing (i.e. a < ,`' < ` order isomorphism, recalling that ` ``' < ` is the "greater than" relation). This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n 
|- ( ph -> N e. NN )
erdsze.f 
|- ( ph -> F : ( 1 ... N ) -1-1-> RR )
erdsze.r 
|- ( ph -> R e. NN )
erdsze.s 
|- ( ph -> S e. NN )
erdsze.l 
|- ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
Assertion erdsze 
|- ( ph -> E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n 
 |-  ( ph -> N e. NN )
2 erdsze.f 
 |-  ( ph -> F : ( 1 ... N ) -1-1-> RR )
3 erdsze.r 
 |-  ( ph -> R e. NN )
4 erdsze.s 
 |-  ( ph -> S e. NN )
5 erdsze.l 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
6 reseq2 
 |-  ( w = y -> ( F |` w ) = ( F |` y ) )
7 isoeq1 
 |-  ( ( F |` w ) = ( F |` y ) -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( w , ( F " w ) ) ) )
8 6 7 syl 
 |-  ( w = y -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( w , ( F " w ) ) ) )
9 isoeq4 
 |-  ( w = y -> ( ( F |` y ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " w ) ) ) )
10 imaeq2 
 |-  ( w = y -> ( F " w ) = ( F " y ) )
11 isoeq5 
 |-  ( ( F " w ) = ( F " y ) -> ( ( F |` y ) Isom < , < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) )
12 10 11 syl 
 |-  ( w = y -> ( ( F |` y ) Isom < , < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) )
13 8 9 12 3bitrd 
 |-  ( w = y -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) )
14 elequ2 
 |-  ( w = y -> ( z e. w <-> z e. y ) )
15 13 14 anbi12d 
 |-  ( w = y -> ( ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) <-> ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) ) )
16 15 cbvrabv 
 |-  { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) }
17 oveq2 
 |-  ( z = x -> ( 1 ... z ) = ( 1 ... x ) )
18 17 pweqd 
 |-  ( z = x -> ~P ( 1 ... z ) = ~P ( 1 ... x ) )
19 elequ1 
 |-  ( z = x -> ( z e. y <-> x e. y ) )
20 19 anbi2d 
 |-  ( z = x -> ( ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) <-> ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) ) )
21 18 20 rabeqbidv 
 |-  ( z = x -> { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } )
22 16 21 syl5eq 
 |-  ( z = x -> { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } )
23 22 imaeq2d 
 |-  ( z = x -> ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) = ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) )
24 23 supeq1d 
 |-  ( z = x -> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) = sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
25 24 cbvmptv 
 |-  ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
26 isoeq1 
 |-  ( ( F |` w ) = ( F |` y ) -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( w , ( F " w ) ) ) )
27 6 26 syl 
 |-  ( w = y -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( w , ( F " w ) ) ) )
28 isoeq4 
 |-  ( w = y -> ( ( F |` y ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " w ) ) ) )
29 isoeq5 
 |-  ( ( F " w ) = ( F " y ) -> ( ( F |` y ) Isom < , `' < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) )
30 10 29 syl 
 |-  ( w = y -> ( ( F |` y ) Isom < , `' < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) )
31 27 28 30 3bitrd 
 |-  ( w = y -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) )
32 31 14 anbi12d 
 |-  ( w = y -> ( ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) <-> ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) ) )
33 32 cbvrabv 
 |-  { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) }
34 19 anbi2d 
 |-  ( z = x -> ( ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) <-> ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) ) )
35 18 34 rabeqbidv 
 |-  ( z = x -> { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } )
36 33 35 syl5eq 
 |-  ( z = x -> { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } )
37 36 imaeq2d 
 |-  ( z = x -> ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) = ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) )
38 37 supeq1d 
 |-  ( z = x -> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) = sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
39 38 cbvmptv 
 |-  ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
40 eqid 
 |-  ( n e. ( 1 ... N ) |-> <. ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) , ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) >. ) = ( n e. ( 1 ... N ) |-> <. ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) , ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) >. )
41 1 2 25 39 40 3 4 5 erdszelem11 
 |-  ( ph -> E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )