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	$⊢ φ \to N \in ℕ$
	erdsze.f	$⊢ φ \to F : (1 \dots N) \underset{1-1}{⟶} ℝ$
	erdsze.r	$⊢ φ \to R \in ℕ$
	erdsze.s	$⊢ φ \to S \in ℕ$
	erdsze.l	$⊢ φ \to (R - 1) (S - 1) < N$
Assertion	erdsze	$⊢ φ \to \exists s \in 𝒫 (1 \dots N) ((R \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <} (s, F [s])) \lor (S \leq \|s\| \land ({F ↾}_{s}) {Isom}_{<, <^{-1}} (s, F [s])))$

Proof

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

Metamath Proof Explorer

Theorem erdsze

Proof