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 eqtrid ⊒ ( 𝑧 = π‘₯ β†’ { 𝑀 ∈ 𝒫 ( 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 eqtrid ⊒ ( 𝑧 = π‘₯ β†’ { 𝑀 ∈ 𝒫 ( 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 < , β—‘ < ( 𝑠 , ( 𝐹 β€œ 𝑠 ) ) ) ) )