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	$$⊢\phi \to N\in \mathbb{N}$$
	erdsze.f	$$⊢\phi \to F:\left(1\dots N\right)\underset{1-1}{⟶}ℝ$$
	erdsze.r	$$⊢\phi \to R\in \mathbb{N}$$
	erdsze.s	$$⊢\phi \to S\in \mathbb{N}$$
	erdsze.l	$$⊢\phi \to \left(R-1\right)\left(S-1\right)<N$$
Assertion	erdsze	$$⊢\phi \to \exists s\in 𝒫\left(1\dots N\right)\left(\left(R\le \left|s\right|\wedge \left({F\upharpoonright }_s\right){Isom}_{<,<}\left(s,F\left[s\right]\right)\right)\vee \left(S\le \left|s\right|\wedge \left({F\upharpoonright }_s\right){Isom}_{<,{<}^{-1}}\left(s,F\left[s\right]\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		erdsze.n	$$⊢\phi \to N\in \mathbb{N}$$
2		erdsze.f	$$⊢\phi \to F:\left(1\dots N\right)\underset{1-1}{⟶}ℝ$$
3		erdsze.r	$$⊢\phi \to R\in \mathbb{N}$$
4		erdsze.s	$$⊢\phi \to S\in \mathbb{N}$$
5		erdsze.l	$$⊢\phi \to \left(R-1\right)\left(S-1\right)<N$$
6		reseq2	$$⊢w=y\to {F\upharpoonright }_w={F\upharpoonright }_y$$
7		isoeq1	$$⊢{F\upharpoonright }_w={F\upharpoonright }_y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\right)$$
8	6 7	syl	$$⊢w=y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\right)$$
9		isoeq4	$$⊢w=y\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[w\right]\right)\right)$$
10		imaeq2	$$⊢w=y\to F\left[w\right]=F\left[y\right]$$
11		isoeq5	$$⊢F\left[w\right]=F\left[y\right]\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\right)$$
12	10 11	syl	$$⊢w=y\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\right)$$
13	8 9 12	3bitrd	$$⊢w=y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\right)$$
14		elequ2	$$⊢w=y\to \left(z\in w\leftrightarrow z\in y\right)$$
15	13 14	anbi12d	$$⊢w=y\to \left(\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\leftrightarrow \left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right)$$
16	15	cbvrabv	$$⊢\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}=\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}$$
17		oveq2	$$⊢z=x\to \left(1\dots z\right)=\left(1\dots x\right)$$
18	17	pweqd	$$⊢z=x\to 𝒫\left(1\dots z\right)=𝒫\left(1\dots x\right)$$
19		elequ1	$$⊢z=x\to \left(z\in y\leftrightarrow x\in y\right)$$
20	19	anbi2d	$$⊢z=x\to \left(\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge z\in y\right)\leftrightarrow \left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right)$$
21	18 20	rabeqbidv	$$⊢z=x\to \left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}=\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}$$
22	16 21	eqtrid	$$⊢z=x\to \left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}=\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}$$
23	22	imaeq2d	$$⊢z=x\to \left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right]=\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right]$$
24	23	supeq1d	$$⊢z=x\to sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)=sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)$$
25	24	cbvmptv	$$⊢\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)=\left(x\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,<}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\right)$$
26		isoeq1	$$⊢{F\upharpoonright }_w={F\upharpoonright }_y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\right)$$
27	6 26	syl	$$⊢w=y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\right)$$
28		isoeq4	$$⊢w=y\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[w\right]\right)\right)$$
29		isoeq5	$$⊢F\left[w\right]=F\left[y\right]\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\right)$$
30	10 29	syl	$$⊢w=y\to \left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\right)$$
31	27 28 30	3bitrd	$$⊢w=y\to \left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\leftrightarrow \left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\right)$$
32	31 14	anbi12d	$$⊢w=y\to \left(\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\leftrightarrow \left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right)$$
33	32	cbvrabv	$$⊢\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}=\left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}$$
34	19	anbi2d	$$⊢z=x\to \left(\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge z\in y\right)\leftrightarrow \left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right)$$
35	18 34	rabeqbidv	$$⊢z=x\to \left\{y\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge z\in y\right)\right\}=\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}$$
36	33 35	eqtrid	$$⊢z=x\to \left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}=\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}$$
37	36	imaeq2d	$$⊢z=x\to \left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right]=\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right]$$
38	37	supeq1d	$$⊢z=x\to sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)=sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)$$
39	38	cbvmptv	$$⊢\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)=\left(x\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{y\in 𝒫\left(1\dots x\right)|\left(\left({F\upharpoonright }_y\right){Isom}_{<,{<}^{-1}}\left(y,F\left[y\right]\right)\wedge x\in y\right)\right\}\right],ℝ,<\right)\right)$$
40		eqid	$$⊢\left(n\in \left(1\dots N\right)⟼⟨\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)\left(n\right),\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)\left(n\right)⟩\right)=\left(n\in \left(1\dots N\right)⟼⟨\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,<}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)\left(n\right),\left(z\in \left(1\dots N\right)⟼sup\left(\left|.\right|\left[\left\{w\in 𝒫\left(1\dots z\right)|\left(\left({F\upharpoonright }_w\right){Isom}_{<,{<}^{-1}}\left(w,F\left[w\right]\right)\wedge z\in w\right)\right\}\right],ℝ,<\right)\right)\left(n\right)⟩\right)$$
41	1 2 25 39 40 3 4 5	erdszelem11	$$⊢\phi \to \exists s\in 𝒫\left(1\dots N\right)\left(\left(R\le \left|s\right|\wedge \left({F\upharpoonright }_s\right){Isom}_{<,<}\left(s,F\left[s\right]\right)\right)\vee \left(S\le \left|s\right|\wedge \left({F\upharpoonright }_s\right){Isom}_{<,{<}^{-1}}\left(s,F\left[s\right]\right)\right)\right)$$