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 ⊢ φ → R ∈ ℕ
erdsze2.s ⊢ φ → S ∈ ℕ
erdsze2.f ⊢ φ → F : A ⟶ 1-1 ℝ
erdsze2.a ⊢ φ → A ⊆ ℝ
erdsze2.l ⊢ φ → R − 1 ⁢ S − 1 < A
Assertion erdsze2 ⊢ φ → ∃ s ∈ 𝒫 A R ≤ s ∧ F ↾ s Isom < , < s F s ∨ S ≤ s ∧ F ↾ s Isom < , < -1 s F s

Proof

Step Hyp Ref Expression
1 erdsze2.r ⊢ φ → R ∈ ℕ
2 erdsze2.s ⊢ φ → S ∈ ℕ
3 erdsze2.f ⊢ φ → F : A ⟶ 1-1 ℝ
4 erdsze2.a ⊢ φ → A ⊆ ℝ
5 erdsze2.l ⊢ φ → R − 1 ⁢ S − 1 < A
6 eqid ⊢ R − 1 ⁢ S − 1 = R − 1 ⁢ S − 1
7 1 2 3 4 6 5 erdsze2lem1 ⊢ φ → ∃ f f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f
8 1 adantr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → R ∈ ℕ
9 2 adantr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → S ∈ ℕ
10 3 adantr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → F : A ⟶ 1-1 ℝ
11 4 adantr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → A ⊆ ℝ
12 5 adantr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → R − 1 ⁢ S − 1 < A
13 simprl ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A
14 simprr ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f
15 8 9 10 11 6 12 13 14 erdsze2lem2 ⊢ φ ∧ f : 1 … R − 1 ⁢ S − 1 + 1 ⟶ 1-1 A ∧ f Isom < , < 1 … R − 1 ⁢ S − 1 + 1 ran ⁡ f → ∃ s ∈ 𝒫 A R ≤ s ∧ F ↾ s Isom < , < s F s ∨ S ≤ s ∧ F ↾ s Isom < , < -1 s F s
16 7 15 exlimddv ⊢ φ → ∃ s ∈ 𝒫 A R ≤ s ∧ F ↾ s Isom < , < s F s ∨ S ≤ s ∧ F ↾ s Isom < , < -1 s F s