Metamath Proof Explorer

Theorem erdszelem11

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
erdszelem.i ⊢ 𝐼 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.j ⊢ 𝐽 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
erdszelem.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ )
erdszelem.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
erdszelem.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
erdszelem.m ⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < 𝑁 )
Assertion erdszelem11 ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 erdsze.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
3 erdszelem.i ⊢ 𝐼 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
4 erdszelem.j ⊢ 𝐽 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ sup ( ( ♯ “ { 𝑦 ∈ 𝒫 ( 1 ... 𝑥 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , ◡ < ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝑥 ∈ 𝑦 ) } ) , ℝ , < ) )
5 erdszelem.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑁 ) ↦ ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ )
6 erdszelem.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
7 erdszelem.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
8 erdszelem.m ⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) < 𝑁 )
9 1 2 3 4 5 6 7 8 erdszelem10 ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → 𝑁 ∈ ℕ )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
12 ltso ⊢ < Or ℝ
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → 𝑚 ∈ ( 1 ... 𝑁 ) )
14 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → 𝑅 ∈ ℕ )
15 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) )
16 10 11 3 12 13 14 15 erdszelem7 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ) ) → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) )
17 16 expr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → 𝑁 ∈ ℕ )
19 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → 𝐹 : ( 1 ... 𝑁 ) –1-1→ ℝ )
20 gtso ⊢ ◡ < Or ℝ
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → 𝑚 ∈ ( 1 ... 𝑁 ) )
22 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → 𝑆 ∈ ℕ )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) )
24 18 19 4 20 21 22 23 erdszelem7 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 1 ... 𝑁 ) ∧ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) )
25 24 expr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
26 17 25 orim12d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) → ( ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ) )
27 26 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) → ( ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ) )
28 9 27 mpd ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
29 r19.43 ⊢ ( ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) ↔ ( ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )
30 28 29 sylibr ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝑅 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ∨ ( 𝑆 ≤ ( ♯ ‘ 𝑠 ) ∧ ( 𝐹 ↾ 𝑠 ) Isom < , ◡ < ( 𝑠 , ( 𝐹 “ 𝑠 ) ) ) ) )