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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
erdsze.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
erdsze.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
erdsze.l ⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < 𝑁 )
Assertion erdsze ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
3 erdsze.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
4 erdsze.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
5 erdsze.l ⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < 𝑁 )
6 reseq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ↾ 𝑤 ) = ( 𝐹 ↾ 𝑦 ) )
7 isoeq1 ⊢ ( ( 𝐹 ↾ 𝑤 ) = ( 𝐹 ↾ 𝑦 ) → ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ) )
8 6 7 syl ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ) )
9 isoeq4 ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ) )
10 imaeq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑦 ) )
11 isoeq5 ⊢ ( ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
12 10 11 syl ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
13 8 9 12 3bitrd ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
14 elequ2 ⊢ ( 𝑤 = 𝑦 → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦 ) )
15 13 14 anbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) ↔ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) ) )
16 15 cbvrabv ⊢ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) }
17 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 1 ... 𝑧 ) = ( 1 ... 𝑥 ) )
18 17 pweqd ⊢ ( 𝑧 = 𝑥 → 𝒫 ( 1 ... 𝑧 ) = 𝒫 ( 1 ... 𝑥 ) )
19 elequ1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
20 19 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) ↔ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) ) )
21 18 20 rabeqbidv ⊢ ( 𝑧 = 𝑥 → { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } )
22 16 21 syl5eq ⊢ ( 𝑧 = 𝑥 → { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } )
23 22 imaeq2d ⊢ ( 𝑧 = 𝑥 → ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) = ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) )
24 23 supeq1d ⊢ ( 𝑧 = 𝑥 → sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
25 24 cbvmptv ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
26 isoeq1 ⊢ ( ( 𝐹 ↾ 𝑤 ) = ( 𝐹 ↾ 𝑦 ) → ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ) )
27 6 26 syl ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ) )
28 isoeq4 ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ) )
29 isoeq5 ⊢ ( ( 𝐹 “ 𝑤 ) = ( 𝐹 “ 𝑦 ) → ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
30 10 29 syl ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
31 27 28 30 3bitrd ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ↔ ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ) )
32 31 14 anbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) ↔ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) ) )
33 32 cbvrabv ⊢ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) }
34 19 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) ↔ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) ) )
35 18 34 rabeqbidv ⊢ ( 𝑧 = 𝑥 → { 𝑦 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑧 ∈ 𝑦 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } )
36 33 35 syl5eq ⊢ ( 𝑧 = 𝑥 → { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } = { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } )
37 36 imaeq2d ⊢ ( 𝑧 = 𝑥 → ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) = ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) )
38 37 supeq1d ⊢ ( 𝑧 = 𝑥 → sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) = sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
39 38 cbvmptv ⊢ ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
40 eqid ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) ‘ 𝑛 ) , ( ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) ‘ 𝑛 ) ⟩ ) = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) ‘ 𝑛 ) , ( ( 𝑧 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑤 ∈ 𝒫 ( 1 ... 𝑧 ) ∣ ( ( 𝐹 ↾ 𝑤 ) Isom < , ◡ < ( 𝑤 , ( 𝐹 “ 𝑤 ) ) ∧ 𝑧 ∈ 𝑤 ) } ) , ℝ , < ) ) ‘ 𝑛 ) ⟩ )
41 1 2 25 39 40 3 4 5 erdszelem11 ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )