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∈𝒫AR≤s∧F↾sIsom<,<sFs∨S≤s∧F↾sIsom<,<-1sFs

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 ⊢φ→∃ff:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f
8 1 adantr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→R∈ℕ
9 2 adantr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→S∈ℕ
10 3 adantr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→F:A⟶1-1ℝ
11 4 adantr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→A⊆ℝ
12 5 adantr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→R−1⁢S−1<A
13 simprl ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→f:1…R−1⁢S−1+1⟶1-1A
14 simprr ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→fIsom<,<1…R−1⁢S−1+1ran⁡f
15 8 9 10 11 6 12 13 14 erdsze2lem2 ⊢φ∧f:1…R−1⁢S−1+1⟶1-1A∧fIsom<,<1…R−1⁢S−1+1ran⁡f→∃s∈𝒫AR≤s∧F↾sIsom<,<sFs∨S≤s∧F↾sIsom<,<-1sFs
16 7 15 exlimddv ⊢φ→∃s∈𝒫AR≤s∧F↾sIsom<,<sFs∨S≤s∧F↾sIsom<,<-1sFs