Metamath Proof Explorer

Theorem erdsze2

Description: Generalize the statement of the Erdős-Szekeres theorem erdsze to "sequences" indexed by an arbitrary subset of RR , which can be infinite. This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 erdsze2.r 
 |-  ( ph -> R e. NN )
2 erdsze2.s 
 |-  ( ph -> S e. NN )
3 erdsze2.f 
 |-  ( ph -> F : A -1-1-> RR )
4 erdsze2.a 
 |-  ( ph -> A C_ RR )
5 erdsze2.l 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < ( # ` A ) )
6 eqid 
 |-  ( ( R - 1 ) x. ( S - 1 ) ) = ( ( R - 1 ) x. ( S - 1 ) )
7 1 2 3 4 6 5 erdsze2lem1 
 |-  ( ph -> E. f ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) )
8 1 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> R e. NN )
9 2 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> S e. NN )
10 3 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> F : A -1-1-> RR )
11 4 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> A C_ RR )
12 5 adantr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> ( ( R - 1 ) x. ( S - 1 ) ) < ( # ` A ) )
13 simprl 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A )
14 simprr 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) )
15 8 9 10 11 6 12 13 14 erdsze2lem2 
 |-  ( ( ph /\ ( f : ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( ( ( R - 1 ) x. ( S - 1 ) ) + 1 ) ) , ran f ) ) ) -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )
16 7 15 exlimddv 
 |-  ( ph -> E. s e. ~P A ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) )