Metamath Proof Explorer

Theorem ramub1

Description: Inductive step for Ramsey's theorem, in the form of an explicit upper bound. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
Assertion ramub1 ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
3 ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
4 ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
6 ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
7 eqid ⊢ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
8 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
9 nnssnn0 ⊢ ℕ ⊆ ℕ0
10 fss ⊢ ( ( 𝐹 : 𝑅 ⟶ ℕ ∧ ℕ ⊆ ℕ0 ) → 𝐹 : 𝑅 ⟶ ℕ0 )
11 3 9 10 sylancl ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
12 peano2nn0 ⊢ ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 → ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∈ ℕ0 )
13 6 12 syl ⊢ ( 𝜑 → ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∈ ℕ0 )
14 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
16 nn0p1nn ⊢ ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 → ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∈ ℕ )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∈ ℕ )
18 14 17 eqeltrd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ )
19 18 nnnn0d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
20 hashclb ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ Fin ↔ ( ♯ ‘ 𝑠 ) ∈ ℕ0 ) )
21 20 elv ⊢ ( 𝑠 ∈ Fin ↔ ( ♯ ‘ 𝑠 ) ∈ ℕ0 )
22 19 21 sylibr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → 𝑠 ∈ Fin )
23 hashnncl ⊢ ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ( ♯ ‘ 𝑠 ) ∈ ℕ ↔ 𝑠 ≠ ∅ ) )
25 18 24 mpbid ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → 𝑠 ≠ ∅ )
26 n0 ⊢ ( 𝑠 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑠 )
27 25 26 sylib ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑤 𝑤 ∈ 𝑠 )
28 1 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝑀 ∈ ℕ )
29 2 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝑅 ∈ Fin )
30 3 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝐹 : 𝑅 ⟶ ℕ )
31 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝐺 : 𝑅 ⟶ ℕ0 )
32 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
33 22 adantrr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝑠 ∈ Fin )
34 simprll ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
35 simprlr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 )
36 simprr ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → 𝑤 ∈ 𝑠 )
37 uneq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 ∪ { 𝑤 } ) = ( 𝑢 ∪ { 𝑤 } ) )
38 37 fveq2d ⊢ ( 𝑣 = 𝑢 → ( 𝑓 ‘ ( 𝑣 ∪ { 𝑤 } ) ) = ( 𝑓 ‘ ( 𝑢 ∪ { 𝑤 } ) ) )
39 38 cbvmptv ⊢ ( 𝑣 ∈ ( ( 𝑠 ∖ { 𝑤 } ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) ( 𝑀 − 1 ) ) ↦ ( 𝑓 ‘ ( 𝑣 ∪ { 𝑤 } ) ) ) = ( 𝑢 ∈ ( ( 𝑠 ∖ { 𝑤 } ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) ( 𝑀 − 1 ) ) ↦ ( 𝑓 ‘ ( 𝑢 ∪ { 𝑤 } ) ) )
40 28 29 30 4 31 32 7 33 34 35 36 39 ramub1lem2 ⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ∧ 𝑤 ∈ 𝑠 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
41 40 expr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( 𝑤 ∈ 𝑠 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
42 41 exlimdv ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ( ∃ 𝑤 𝑤 ∈ 𝑠 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
43 27 42 mpd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝑠 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
44 7 8 2 11 13 43 ramub2 ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )