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 ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → ( 𝑀 Ramsey 𝐹 ) = 0 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2 simpl1 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → 𝑀 ∈ ℕ )
3 2 nnnn0d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → 𝑀 ∈ ℕ0 )
4 simpl2 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → 𝑅 ∈ 𝑉 )
5 simpl3 ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → 𝐹 : 𝑅 ⟶ ℕ0 )
6 0nn0 ⊢ 0 ∈ ℕ0
7 6 a1i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → 0 ∈ ℕ0 )
8 simplrl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → 𝐶 ∈ 𝑅 )
9 0elpw ⊢ ∅ ∈ 𝒫 𝑠
10 9 a1i ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ∅ ∈ 𝒫 𝑠 )
11 simplrr ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) = 0 )
12 0le0 ⊢ 0 ≤ 0
13 11 12 eqbrtrdi ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( 𝐹 ‘ 𝐶 ) ≤ 0 )
14 simpll1 ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → 𝑀 ∈ ℕ )
15 1 0hashbc ⊢ ( 𝑀 ∈ ℕ → ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) = ∅ )
16 14 15 syl ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) = ∅ )
17 0ss ⊢ ∅ ⊆ ( ◡ 𝑓 “ { 𝐶 } )
18 16 17 eqsstrdi ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) )
19 fveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐶 ) )
20 19 breq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐶 ) ≤ ( ♯ ‘ 𝑥 ) ) )
21 sneq ⊢ ( 𝑐 = 𝐶 → { 𝑐 } = { 𝐶 } )
22 21 imaeq2d ⊢ ( 𝑐 = 𝐶 → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ 𝑓 “ { 𝐶 } ) )
23 22 sseq2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) )
24 20 23 anbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ( ( 𝐹 ‘ 𝐶 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) ) )
25 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
26 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
27 25 26 eqtrdi ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
28 27 breq2d ⊢ ( 𝑥 = ∅ → ( ( 𝐹 ‘ 𝐶 ) ≤ ( ♯ ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐶 ) ≤ 0 ) )
29 oveq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) = ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) )
30 29 sseq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ↔ ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) )
31 28 30 anbi12d ⊢ ( 𝑥 = ∅ → ( ( ( 𝐹 ‘ 𝐶 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) ↔ ( ( 𝐹 ‘ 𝐶 ) ≤ 0 ∧ ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) ) )
32 24 31 rspc2ev ⊢ ( ( 𝐶 ∈ 𝑅 ∧ ∅ ∈ 𝒫 𝑠 ∧ ( ( 𝐹 ‘ 𝐶 ) ≤ 0 ∧ ( ∅ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝐶 } ) ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
33 8 10 13 18 32 syl112anc ⊢ ( ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) ∧ ( 0 ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
34 1 3 4 5 7 33 ramub ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → ( 𝑀 Ramsey 𝐹 ) ≤ 0 )
35 ramubcl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ ( 𝑀 Ramsey 𝐹 ) ≤ 0 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
36 3 4 5 7 34 35 syl32anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
37 nn0le0eq0 ⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 → ( ( 𝑀 Ramsey 𝐹 ) ≤ 0 ↔ ( 𝑀 Ramsey 𝐹 ) = 0 ) )
38 36 37 syl ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → ( ( 𝑀 Ramsey 𝐹 ) ≤ 0 ↔ ( 𝑀 Ramsey 𝐹 ) = 0 ) )
39 34 38 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝐶 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝐶 ) = 0 ) ) → ( 𝑀 Ramsey 𝐹 ) = 0 )