Metamath Proof Explorer

Theorem erdszelem10

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 erdszelem10 ( 𝜑 → ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) )

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 fzfi ⊢ ( 1 ... ( 𝑅 − 1 ) ) ∈ Fin
10 fzfi ⊢ ( 1 ... ( 𝑆 − 1 ) ) ∈ Fin
11 xpfi ⊢ ( ( ( 1 ... ( 𝑅 − 1 ) ) ∈ Fin ∧ ( 1 ... ( 𝑆 − 1 ) ) ∈ Fin ) → ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ∈ Fin )
12 9 10 11 mp2an ⊢ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ∈ Fin
13 ssdomg ⊢ ( ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ∈ Fin → ( ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) → ran 𝑇 ≼ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
14 12 13 ax-mp ⊢ ( ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) → ran 𝑇 ≼ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) )
15 domnsym ⊢ ( ran 𝑇 ≼ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) → ¬ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ran 𝑇 )
16 14 15 syl ⊢ ( ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) → ¬ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ran 𝑇 )
17 hashxp ⊢ ( ( ( 1 ... ( 𝑅 − 1 ) ) ∈ Fin ∧ ( 1 ... ( 𝑆 − 1 ) ) ∈ Fin ) → ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) = ( ( ♯ ‘ ( 1 ... ( 𝑅 − 1 ) ) ) · ( ♯ ‘ ( 1 ... ( 𝑆 − 1 ) ) ) ) )
18 9 10 17 mp2an ⊢ ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) = ( ( ♯ ‘ ( 1 ... ( 𝑅 − 1 ) ) ) · ( ♯ ‘ ( 1 ... ( 𝑆 − 1 ) ) ) )
19 nnm1nn0 ⊢ ( 𝑅 ∈ ℕ → ( 𝑅 − 1 ) ∈ ℕ0 )
20 hashfz1 ⊢ ( ( 𝑅 − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑅 − 1 ) ) ) = ( 𝑅 − 1 ) )
21 6 19 20 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑅 − 1 ) ) ) = ( 𝑅 − 1 ) )
22 nnm1nn0 ⊢ ( 𝑆 ∈ ℕ → ( 𝑆 − 1 ) ∈ ℕ0 )
23 hashfz1 ⊢ ( ( 𝑆 − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑆 − 1 ) ) ) = ( 𝑆 − 1 ) )
24 7 22 23 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑆 − 1 ) ) ) = ( 𝑆 − 1 ) )
25 21 24 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... ( 𝑅 − 1 ) ) ) · ( ♯ ‘ ( 1 ... ( 𝑆 − 1 ) ) ) ) = ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) )
26 18 25 syl5eq ⊢ ( 𝜑 → ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) = ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) )
27 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
28 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
29 27 28 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
30 8 26 29 3brtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) < ( ♯ ‘ ( 1 ... 𝑁 ) ) )
31 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
32 hashsdom ⊢ ( ( ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) < ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ( 1 ... 𝑁 ) ) )
33 12 31 32 sylancr ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) < ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ( 1 ... 𝑁 ) ) )
34 30 33 mpbid ⊢ ( 𝜑 → ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ( 1 ... 𝑁 ) )
35 1 2 3 4 5 erdszelem9 ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) )
36 f1f1orn ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) → 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ran 𝑇 )
37 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
38 37 f1oen ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1-onto→ ran 𝑇 → ( 1 ... 𝑁 ) ≈ ran 𝑇 )
39 35 36 38 3syl ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ≈ ran 𝑇 )
40 sdomentr ⊢ ( ( ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ( 1 ... 𝑁 ) ∧ ( 1 ... 𝑁 ) ≈ ran 𝑇 ) → ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ran 𝑇 )
41 34 39 40 syl2anc ⊢ ( 𝜑 → ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ≺ ran 𝑇 )
42 16 41 nsyl3 ⊢ ( 𝜑 → ¬ ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) )
43 nss ⊢ ( ¬ ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ ran 𝑇 ∧ ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
44 df-rex ⊢ ( ∃ 𝑠 ∈ ran 𝑇 ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑠 ( 𝑠 ∈ ran 𝑇 ∧ ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
45 43 44 bitr4i ⊢ ( ¬ ran 𝑇 ⊆ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑠 ∈ ran 𝑇 ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) )
46 42 45 sylib ⊢ ( 𝜑 → ∃ 𝑠 ∈ ran 𝑇 ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) )
47 f1fn ⊢ ( 𝑇 : ( 1 ... 𝑁 ) –1-1→ ( ℕ × ℕ ) → 𝑇 Fn ( 1 ... 𝑁 ) )
48 eleq1 ⊢ ( 𝑠 = ( 𝑇 ‘ 𝑚 ) → ( 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
49 48 notbid ⊢ ( 𝑠 = ( 𝑇 ‘ 𝑚 ) → ( ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
50 49 rexrn ⊢ ( 𝑇 Fn ( 1 ... 𝑁 ) → ( ∃ 𝑠 ∈ ran 𝑇 ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
51 35 47 50 3syl ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ran 𝑇 ¬ 𝑠 ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
52 46 51 mpbid ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) )
53 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐼 ‘ 𝑛 ) = ( 𝐼 ‘ 𝑚 ) )
54 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐽 ‘ 𝑛 ) = ( 𝐽 ‘ 𝑚 ) )
55 53 54 opeq12d ⊢ ( 𝑛 = 𝑚 → ⟨ ( 𝐼 ‘ 𝑛 ) , ( 𝐽 ‘ 𝑛 ) ⟩ = ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ )
56 opex ⊢ ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ ∈ V
57 55 5 56 fvmpt ⊢ ( 𝑚 ∈ ( 1 ... 𝑁 ) → ( 𝑇 ‘ 𝑚 ) = ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑚 ) = ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ )
59 58 eleq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ) )
60 opelxp ⊢ ( ⟨ ( 𝐼 ‘ 𝑚 ) , ( 𝐽 ‘ 𝑚 ) ⟩ ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ( ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) )
61 59 60 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ( ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) )
62 61 notbid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ¬ ( ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) )
63 ianor ⊢ ( ¬ ( ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) )
64 62 63 bitrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑁 ) ) → ( ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) )
65 64 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ¬ ( 𝑇 ‘ 𝑚 ) ∈ ( ( 1 ... ( 𝑅 − 1 ) ) × ( 1 ... ( 𝑆 − 1 ) ) ) ↔ ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) ) )
66 52 65 mpbid ⊢ ( 𝜑 → ∃ 𝑚 ∈ ( 1 ... 𝑁 ) ( ¬ ( 𝐼 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑅 − 1 ) ) ∨ ¬ ( 𝐽 ‘ 𝑚 ) ∈ ( 1 ... ( 𝑆 − 1 ) ) ) )