Metamath Proof Explorer

Theorem ramlb

Description: Establish a lower bound on a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses ramlb.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
ramlb.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
ramlb.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
ramlb.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
ramlb.s ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ramlb.g ⊢ ( 𝜑 → 𝐺 : ( ( 1 ... 𝑁 ) 𝐶 𝑀 ) ⟶ 𝑅 )
ramlb.i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ( ♯ ‘ 𝑥 ) < ( 𝐹 ‘ 𝑐 ) ) )
Assertion ramlb ( 𝜑 → 𝑁 < ( 𝑀 Ramsey 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ramlb.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2 ramlb.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 ramlb.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 ramlb.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
5 ramlb.s ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 ramlb.g ⊢ ( 𝜑 → 𝐺 : ( ( 1 ... 𝑁 ) 𝐶 𝑀 ) ⟶ 𝑅 )
7 ramlb.i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ( ♯ ‘ 𝑥 ) < ( 𝐹 ‘ 𝑐 ) ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
9 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → 𝑅 ∈ 𝑉 )
10 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → 𝐹 : 𝑅 ⟶ ℕ0 )
11 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → 𝑁 ∈ ℕ0 )
12 simpr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 )
13 ramubcl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
14 8 9 10 11 12 13 syl32anc ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
15 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ( 1 ... 𝑁 ) ∈ Fin )
16 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
17 5 16 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
18 17 breq2d ⊢ ( 𝜑 → ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) )
19 18 biimpar ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ ( 1 ... 𝑁 ) ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → 𝐺 : ( ( 1 ... 𝑁 ) 𝐶 𝑀 ) ⟶ 𝑅 )
21 1 8 9 10 14 15 19 20 rami ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
22 elpwi ⊢ ( 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) → 𝑥 ⊆ ( 1 ... 𝑁 ) )
23 7 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ( ♯ ‘ 𝑥 ) < ( 𝐹 ‘ 𝑐 ) ) )
24 fzfid ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
25 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → 𝑥 ⊆ ( 1 ... 𝑁 ) )
26 24 25 ssfid ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → 𝑥 ∈ Fin )
27 hashcl ⊢ ( 𝑥 ∈ Fin → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
28 26 27 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
29 28 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ♯ ‘ 𝑥 ) ∈ ℝ )
30 simpl ⊢ ( ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) → 𝑐 ∈ 𝑅 )
31 ffvelrn ⊢ ( ( 𝐹 : 𝑅 ⟶ ℕ0 ∧ 𝑐 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 )
32 10 30 31 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 )
33 32 nn0red ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℝ )
34 29 33 ltnled ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( ♯ ‘ 𝑥 ) < ( 𝐹 ‘ 𝑐 ) ↔ ¬ ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ) )
35 23 34 sylibd ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ ( 1 ... 𝑁 ) ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ¬ ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ) )
36 22 35 sylanr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ) ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) → ¬ ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ) )
37 36 con2d ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ) ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) → ¬ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
38 imnan ⊢ ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) → ¬ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ↔ ¬ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
39 37 38 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ) ) → ¬ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
40 39 pm2.21d ⊢ ( ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) → ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) )
41 40 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 ( 1 ... 𝑁 ) ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) → ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) )
42 21 41 mpd ⊢ ( ( 𝜑 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) → ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 )
43 42 pm2.01da ⊢ ( 𝜑 → ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 )
44 5 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
45 44 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
46 ramxrcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℝ* )
47 2 3 4 46 syl3anc ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ∈ ℝ* )
48 xrltnle ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( 𝑀 Ramsey 𝐹 ) ∈ ℝ* ) → ( 𝑁 < ( 𝑀 Ramsey 𝐹 ) ↔ ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) )
49 45 47 48 syl2anc ⊢ ( 𝜑 → ( 𝑁 < ( 𝑀 Ramsey 𝐹 ) ↔ ¬ ( 𝑀 Ramsey 𝐹 ) ≤ 𝑁 ) )
50 43 49 mpbird ⊢ ( 𝜑 → 𝑁 < ( 𝑀 Ramsey 𝐹 ) )