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 ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
erdsze2.l ⊒ ( πœ‘ β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) < ( β™― β€˜ 𝐴 ) )
Assertion erdsze2 ( πœ‘ β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
2 erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
3 erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
4 erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
5 erdsze2.l ⊒ ( πœ‘ β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) < ( β™― β€˜ 𝐴 ) )
6 eqid ⊒ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) = ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) )
7 1 2 3 4 6 5 erdsze2lem1 ⊒ ( πœ‘ β†’ βˆƒ 𝑓 ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) )
8 1 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝑅 ∈ β„• )
9 2 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝑆 ∈ β„• )
10 3 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
11 4 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝐴 βŠ† ℝ )
12 5 adantr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) < ( β™― β€˜ 𝐴 ) )
13 simprl ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 )
14 simprr ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) )
15 8 9 10 11 6 12 13 14 erdsze2lem2 ⊒ ( ( πœ‘ ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )
16 7 15 exlimddv ⊒ ( πœ‘ β†’ βˆƒ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ∨ ( 𝑆 ≀ ( β™― β€˜ 𝑠 ) ∧ ( 𝐹 β†Ύ 𝑠 ) Isom < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )