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	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	erdsze2.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
	erdsze2.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ ℝ )
	erdsze2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	erdsze2.l	⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < ( ♯ ‘ 𝐴 ) )
Assertion	erdsze2	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		erdsze2.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2		erdsze2.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3		erdsze2.f	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ ℝ )
4		erdsze2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
5		erdsze2.l	⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < ( ♯ ‘ 𝐴 ) )
6		eqid	⊢ ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) = ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) )
7	1 2 3 4 6 5	erdsze2lem1	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝑅 ∈ ℕ )
9	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝑆 ∈ ℕ )
10	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝐹 : 𝐴 –1-1→ ℝ )
11	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝐴 ⊆ ℝ )
12	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < ( ♯ ‘ 𝐴 ) )
13		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 )
14		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) )
15	8 9 10 11 6 12 13 14	erdsze2lem2	⊢ ( ( 𝜑 ∧ ( 𝑓 : ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) + 1 ) ) , ran 𝑓 ) ) ) → ∃ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
16	7 15	exlimddv	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝒫 𝐴 ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )