Metamath Proof Explorer

Theorem ram0

Description: The Ramsey number when R = (/) . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ram0 ⊢ M ∈ ℕ 0 → M Ramsey ∅ = M

Proof

Step Hyp Ref Expression
1 eqid ⊢ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 id ⊢ M ∈ ℕ 0 → M ∈ ℕ 0
3 0ex ⊢ ∅ ∈ V
4 3 a1i ⊢ M ∈ ℕ 0 → ∅ ∈ V
5 f0 ⊢ ∅ : ∅ ⟶ ℕ 0
6 5 a1i ⊢ M ∈ ℕ 0 → ∅ : ∅ ⟶ ℕ 0
7 f00 ⊢ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ ∅ ↔ f = ∅ ∧ s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
8 vex ⊢ s ∈ V
9 simpl ⊢ M ∈ ℕ 0 ∧ M ≤ s → M ∈ ℕ 0
10 1 hashbcval ⊢ s ∈ V ∧ M ∈ ℕ 0 → s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = x ∈ 𝒫 s | x = M
11 8 9 10 sylancr ⊢ M ∈ ℕ 0 ∧ M ≤ s → s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = x ∈ 𝒫 s | x = M
12 hashfz1 ⊢ M ∈ ℕ 0 → 1 … M = M
13 12 breq1d ⊢ M ∈ ℕ 0 → 1 … M ≤ s ↔ M ≤ s
14 13 biimpar ⊢ M ∈ ℕ 0 ∧ M ≤ s → 1 … M ≤ s
15 fzfid ⊢ M ∈ ℕ 0 ∧ M ≤ s → 1 … M ∈ Fin
16 hashdom ⊢ 1 … M ∈ Fin ∧ s ∈ V → 1 … M ≤ s ↔ 1 … M ≼ s
17 15 8 16 sylancl ⊢ M ∈ ℕ 0 ∧ M ≤ s → 1 … M ≤ s ↔ 1 … M ≼ s
18 14 17 mpbid ⊢ M ∈ ℕ 0 ∧ M ≤ s → 1 … M ≼ s
19 8 domen ⊢ 1 … M ≼ s ↔ ∃ x 1 … M ≈ x ∧ x ⊆ s
20 18 19 sylib ⊢ M ∈ ℕ 0 ∧ M ≤ s → ∃ x 1 … M ≈ x ∧ x ⊆ s
21 simprr ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → x ⊆ s
22 velpw ⊢ x ∈ 𝒫 s ↔ x ⊆ s
23 21 22 sylibr ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → x ∈ 𝒫 s
24 hasheni ⊢ 1 … M ≈ x → 1 … M = x
25 24 ad2antrl ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → 1 … M = x
26 12 ad2antrr ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → 1 … M = M
27 25 26 eqtr3d ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → x = M
28 23 27 jca ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ 1 … M ≈ x ∧ x ⊆ s → x ∈ 𝒫 s ∧ x = M
29 28 ex ⊢ M ∈ ℕ 0 ∧ M ≤ s → 1 … M ≈ x ∧ x ⊆ s → x ∈ 𝒫 s ∧ x = M
30 29 eximdv ⊢ M ∈ ℕ 0 ∧ M ≤ s → ∃ x 1 … M ≈ x ∧ x ⊆ s → ∃ x x ∈ 𝒫 s ∧ x = M
31 20 30 mpd ⊢ M ∈ ℕ 0 ∧ M ≤ s → ∃ x x ∈ 𝒫 s ∧ x = M
32 df-rex ⊢ ∃ x ∈ 𝒫 s x = M ↔ ∃ x x ∈ 𝒫 s ∧ x = M
33 31 32 sylibr ⊢ M ∈ ℕ 0 ∧ M ≤ s → ∃ x ∈ 𝒫 s x = M
34 rabn0 ⊢ x ∈ 𝒫 s | x = M ≠ ∅ ↔ ∃ x ∈ 𝒫 s x = M
35 33 34 sylibr ⊢ M ∈ ℕ 0 ∧ M ≤ s → x ∈ 𝒫 s | x = M ≠ ∅
36 11 35 eqnetrd ⊢ M ∈ ℕ 0 ∧ M ≤ s → s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ≠ ∅
37 36 neneqd ⊢ M ∈ ℕ 0 ∧ M ≤ s → ¬ s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
38 37 pm2.21d ⊢ M ∈ ℕ 0 ∧ M ≤ s → s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅ → ∃ c ∈ ∅ ∃ x ∈ 𝒫 s ∅ ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
39 38 adantld ⊢ M ∈ ℕ 0 ∧ M ≤ s → f = ∅ ∧ s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅ → ∃ c ∈ ∅ ∃ x ∈ 𝒫 s ∅ ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
40 7 39 biimtrid ⊢ M ∈ ℕ 0 ∧ M ≤ s → f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ ∅ → ∃ c ∈ ∅ ∃ x ∈ 𝒫 s ∅ ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
41 40 impr ⊢ M ∈ ℕ 0 ∧ M ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ ∅ → ∃ c ∈ ∅ ∃ x ∈ 𝒫 s ∅ ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
42 1 2 4 6 2 41 ramub ⊢ M ∈ ℕ 0 → M Ramsey ∅ ≤ M
43 nnnn0 ⊢ M ∈ ℕ → M ∈ ℕ 0
44 3 a1i ⊢ M ∈ ℕ → ∅ ∈ V
45 5 a1i ⊢ M ∈ ℕ → ∅ : ∅ ⟶ ℕ 0
46 nnm1nn0 ⊢ M ∈ ℕ → M − 1 ∈ ℕ 0
47 f0 ⊢ ∅ : ∅ ⟶ ∅
48 fzfid ⊢ M ∈ ℕ → 1 … M − 1 ∈ Fin
49 1 hashbc2 ⊢ 1 … M − 1 ∈ Fin ∧ M ∈ ℕ 0 → 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ( 1 … M − 1 M)
50 48 43 49 syl2anc ⊢ M ∈ ℕ → 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ( 1 … M − 1 M)
51 hashfz1 ⊢ M − 1 ∈ ℕ 0 → 1 … M − 1 = M − 1
52 46 51 syl ⊢ M ∈ ℕ → 1 … M − 1 = M − 1
53 52 oveq1d ⊢ M ∈ ℕ → ( 1 … M − 1 M) = ( M − 1 M)
54 nnz ⊢ M ∈ ℕ → M ∈ ℤ
55 nnre ⊢ M ∈ ℕ → M ∈ ℝ
56 55 ltm1d ⊢ M ∈ ℕ → M − 1 < M
57 56 olcd ⊢ M ∈ ℕ → M < 0 ∨ M − 1 < M
58 bcval4 ⊢ M − 1 ∈ ℕ 0 ∧ M ∈ ℤ ∧ M < 0 ∨ M − 1 < M → ( M − 1 M) = 0
59 46 54 57 58 syl3anc ⊢ M ∈ ℕ → ( M − 1 M) = 0
60 50 53 59 3eqtrd ⊢ M ∈ ℕ → 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = 0
61 ovex ⊢ 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∈ V
62 hasheq0 ⊢ 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ∈ V → 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = 0 ↔ 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
63 61 62 ax-mp ⊢ 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = 0 ↔ 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
64 60 63 sylib ⊢ M ∈ ℕ → 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
65 64 feq2d ⊢ M ∈ ℕ → ∅ : 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ ∅ ↔ ∅ : ∅ ⟶ ∅
66 47 65 mpbiri ⊢ M ∈ ℕ → ∅ : 1 … M − 1 a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ ∅
67 noel ⊢ ¬ c ∈ ∅
68 67 pm2.21i ⊢ c ∈ ∅ → x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ ∅ -1 c → x < ∅ ⁡ c
69 68 ad2antrl ⊢ M ∈ ℕ ∧ c ∈ ∅ ∧ x ⊆ 1 … M − 1 → x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ ∅ -1 c → x < ∅ ⁡ c
70 1 43 44 45 46 66 69 ramlb ⊢ M ∈ ℕ → M − 1 < M Ramsey ∅
71 ramubcl ⊢ M ∈ ℕ 0 ∧ ∅ ∈ V ∧ ∅ : ∅ ⟶ ℕ 0 ∧ M ∈ ℕ 0 ∧ M Ramsey ∅ ≤ M → M Ramsey ∅ ∈ ℕ 0
72 2 4 6 2 42 71 syl32anc ⊢ M ∈ ℕ 0 → M Ramsey ∅ ∈ ℕ 0
73 nn0lem1lt ⊢ M ∈ ℕ 0 ∧ M Ramsey ∅ ∈ ℕ 0 → M ≤ M Ramsey ∅ ↔ M − 1 < M Ramsey ∅
74 43 72 73 syl2anc2 ⊢ M ∈ ℕ → M ≤ M Ramsey ∅ ↔ M − 1 < M Ramsey ∅
75 70 74 mpbird ⊢ M ∈ ℕ → M ≤ M Ramsey ∅
76 75 a1i ⊢ M ∈ ℕ 0 → M ∈ ℕ → M ≤ M Ramsey ∅
77 72 nn0ge0d ⊢ M ∈ ℕ 0 → 0 ≤ M Ramsey ∅
78 breq1 ⊢ M = 0 → M ≤ M Ramsey ∅ ↔ 0 ≤ M Ramsey ∅
79 77 78 syl5ibrcom ⊢ M ∈ ℕ 0 → M = 0 → M ≤ M Ramsey ∅
80 elnn0 ⊢ M ∈ ℕ 0 ↔ M ∈ ℕ ∨ M = 0
81 80 biimpi ⊢ M ∈ ℕ 0 → M ∈ ℕ ∨ M = 0
82 76 79 81 mpjaod ⊢ M ∈ ℕ 0 → M ≤ M Ramsey ∅
83 72 nn0red ⊢ M ∈ ℕ 0 → M Ramsey ∅ ∈ ℝ
84 nn0re ⊢ M ∈ ℕ 0 → M ∈ ℝ
85 83 84 letri3d ⊢ M ∈ ℕ 0 → M Ramsey ∅ = M ↔ M Ramsey ∅ ≤ M ∧ M ≤ M Ramsey ∅
86 42 82 85 mpbir2and ⊢ M ∈ ℕ 0 → M Ramsey ∅ = M