Metamath Proof Explorer

Theorem ramz2

Description: The Ramsey number when F has value zero for some color C . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion ramz2 ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M Ramsey F = 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
2 simpl1 ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M ∈ ℕ
3 2 nnnn0d ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M ∈ ℕ 0
4 simpl2 ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → R ∈ V
5 simpl3 ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → F : R ⟶ ℕ 0
6 0nn0 ⊢ 0 ∈ ℕ 0
7 6 a1i ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → 0 ∈ ℕ 0
8 simplrl ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → C ∈ R
9 0elpw ⊢ ∅ ∈ 𝒫 s
10 9 a1i ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∅ ∈ 𝒫 s
11 simplrr ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → F ⁡ C = 0
12 0le0 ⊢ 0 ≤ 0
13 11 12 eqbrtrdi ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → F ⁡ C ≤ 0
14 simpll1 ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → M ∈ ℕ
15 1 0hashbc ⊢ M ∈ ℕ → ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
16 14 15 syl ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅
17 0ss ⊢ ∅ ⊆ f -1 C
18 16 17 eqsstrdi ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C
19 fveq2 ⊢ c = C → F ⁡ c = F ⁡ C
20 19 breq1d ⊢ c = C → F ⁡ c ≤ x ↔ F ⁡ C ≤ x
21 sneq ⊢ c = C → c = C
22 21 imaeq2d ⊢ c = C → f -1 c = f -1 C
23 22 sseq2d ⊢ c = C → x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ↔ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C
24 20 23 anbi12d ⊢ c = C → F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c ↔ F ⁡ C ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C
25 fveq2 ⊢ x = ∅ → x = ∅
26 hash0 ⊢ ∅ = 0
27 25 26 eqtrdi ⊢ x = ∅ → x = 0
28 27 breq2d ⊢ x = ∅ → F ⁡ C ≤ x ↔ F ⁡ C ≤ 0
29 oveq1 ⊢ x = ∅ → x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M = ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M
30 29 sseq1d ⊢ x = ∅ → x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C ↔ ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C
31 28 30 anbi12d ⊢ x = ∅ → F ⁡ C ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C ↔ F ⁡ C ≤ 0 ∧ ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C
32 24 31 rspc2ev ⊢ C ∈ R ∧ ∅ ∈ 𝒫 s ∧ F ⁡ C ≤ 0 ∧ ∅ a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 C → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
33 8 10 13 18 32 syl112anc ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 ∧ 0 ≤ s ∧ f : s a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⟶ R → ∃ c ∈ R ∃ x ∈ 𝒫 s F ⁡ c ≤ x ∧ x a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i M ⊆ f -1 c
34 1 3 4 5 7 33 ramub ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M Ramsey F ≤ 0
35 ramubcl ⊢ M ∈ ℕ 0 ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ 0 ∈ ℕ 0 ∧ M Ramsey F ≤ 0 → M Ramsey F ∈ ℕ 0
36 3 4 5 7 34 35 syl32anc ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M Ramsey F ∈ ℕ 0
37 nn0le0eq0 ⊢ M Ramsey F ∈ ℕ 0 → M Ramsey F ≤ 0 ↔ M Ramsey F = 0
38 36 37 syl ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M Ramsey F ≤ 0 ↔ M Ramsey F = 0
39 34 38 mpbid ⊢ M ∈ ℕ ∧ R ∈ V ∧ F : R ⟶ ℕ 0 ∧ C ∈ R ∧ F ⁡ C = 0 → M Ramsey F = 0