Metamath Proof Explorer

Theorem ramcl

Description: Ramsey's theorem: the Ramsey number is an integer for every finite coloring and set of upper bounds. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion ramcl ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 nn0ex ⊢ ℕ0 ∈ V
2 simpr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ) → 𝑅 ∈ Fin )
3 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑅 ∈ Fin ) → ( 𝐹 ∈ ( ℕ0 ↑m 𝑅 ) ↔ 𝐹 : 𝑅 ⟶ ℕ0 ) )
4 1 2 3 sylancr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ) → ( 𝐹 ∈ ( ℕ0 ↑m 𝑅 ) ↔ 𝐹 : 𝑅 ⟶ ℕ0 ) )
5 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 Ramsey 𝑓 ) = ( 0 Ramsey 𝑓 ) )
6 5 eleq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( 0 Ramsey 𝑓 ) ∈ ℕ0 ) )
7 6 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 0 Ramsey 𝑓 ) ∈ ℕ0 ) )
8 7 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ) ↔ ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 0 Ramsey 𝑓 ) ∈ ℕ0 ) ) )
9 oveq1 ⊢ ( 𝑥 = 𝑚 → ( 𝑥 Ramsey 𝑓 ) = ( 𝑚 Ramsey 𝑓 ) )
10 9 eleq1d ⊢ ( 𝑥 = 𝑚 → ( ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ) )
11 10 ralbidv ⊢ ( 𝑥 = 𝑚 → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑚 → ( ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ) ↔ ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ) ) )
13 oveq1 ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( 𝑥 Ramsey 𝑓 ) = ( ( 𝑚 + 1 ) Ramsey 𝑓 ) )
14 13 eleq1d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
15 14 ralbidv ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
16 15 imbi2d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ) ↔ ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
17 oveq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 Ramsey 𝑓 ) = ( 𝑀 Ramsey 𝑓 ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 ) )
19 18 ralbidv ⊢ ( 𝑥 = 𝑀 → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ↔ ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑥 Ramsey 𝑓 ) ∈ ℕ0 ) ↔ ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 ) ) )
21 elmapi ⊢ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) → 𝑓 : 𝑅 ⟶ ℕ0 )
22 0ramcl ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ0 ) → ( 0 Ramsey 𝑓 ) ∈ ℕ0 )
23 21 22 sylan2 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ) → ( 0 Ramsey 𝑓 ) ∈ ℕ0 )
24 23 ralrimiva ⊢ ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 0 Ramsey 𝑓 ) ∈ ℕ0 )
25 oveq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑚 Ramsey 𝑓 ) = ( 𝑚 Ramsey 𝑔 ) )
26 25 eleq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) )
27 26 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ↔ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 )
28 simpll ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → 𝑅 ∈ Fin )
29 21 ad2antrl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → 𝑓 : 𝑅 ⟶ ℕ0 )
30 29 ffvelcdmda ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) ∧ 𝑘 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℕ0 )
31 28 30 fsumnn0cl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ∈ ℕ0 )
32 eqeq2 ⊢ ( 𝑥 = 0 → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ↔ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) )
33 32 anbi2d ⊢ ( 𝑥 = 0 → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) ↔ ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) ) )
34 33 imbi1d ⊢ ( 𝑥 = 0 → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
35 34 albidv ⊢ ( 𝑥 = 0 → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
36 35 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ↔ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
37 eqeq2 ⊢ ( 𝑥 = 𝑛 → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ↔ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) )
38 37 anbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) ↔ ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) ) )
39 38 imbi1d ⊢ ( 𝑥 = 𝑛 → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
40 39 albidv ⊢ ( 𝑥 = 𝑛 → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
41 40 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ↔ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
42 eqeq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ↔ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) )
43 42 anbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) ↔ ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) )
44 43 imbi1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
45 44 albidv ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
46 45 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ↔ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
47 eqeq2 ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ↔ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) )
48 47 anbi2d ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) ↔ ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) ) )
49 48 imbi1d ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
50 49 albidv ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
51 50 imbi2d ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) → ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑥 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ↔ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
52 simplll ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → 𝑅 ∈ Fin )
53 ffvelcdm ⊢ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ 𝑘 ∈ 𝑅 ) → ( ℎ ‘ 𝑘 ) ∈ ℕ0 )
54 53 adantll ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑘 ∈ 𝑅 ) → ( ℎ ‘ 𝑘 ) ∈ ℕ0 )
55 54 nn0red ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑘 ∈ 𝑅 ) → ( ℎ ‘ 𝑘 ) ∈ ℝ )
56 54 nn0ge0d ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑘 ∈ 𝑅 ) → 0 ≤ ( ℎ ‘ 𝑘 ) )
57 52 55 56 fsum00 ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ↔ ∀ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) )
58 fvex ⊢ ( ℎ ‘ 𝑘 ) ∈ V
59 58 rgenw ⊢ ∀ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) ∈ V
60 mpteqb ⊢ ( ∀ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) ∈ V → ( ( 𝑘 ∈ 𝑅 ↦ ( ℎ ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑅 ↦ 0 ) ↔ ∀ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) )
61 59 60 ax-mp ⊢ ( ( 𝑘 ∈ 𝑅 ↦ ( ℎ ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑅 ↦ 0 ) ↔ ∀ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 )
62 57 61 bitr4di ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ↔ ( 𝑘 ∈ 𝑅 ↦ ( ℎ ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑅 ↦ 0 ) ) )
63 simpr ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ℎ : 𝑅 ⟶ ℕ0 )
64 63 feqmptd ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ℎ = ( 𝑘 ∈ 𝑅 ↦ ( ℎ ‘ 𝑘 ) ) )
65 fconstmpt ⊢ ( 𝑅 × { 0 } ) = ( 𝑘 ∈ 𝑅 ↦ 0 )
66 65 a1i ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( 𝑅 × { 0 } ) = ( 𝑘 ∈ 𝑅 ↦ 0 ) )
67 64 66 eqeq12d ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( ℎ = ( 𝑅 × { 0 } ) ↔ ( 𝑘 ∈ 𝑅 ↦ ( ℎ ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑅 ↦ 0 ) ) )
68 62 67 bitr4d ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ↔ ℎ = ( 𝑅 × { 0 } ) ) )
69 xpeq1 ⊢ ( 𝑅 = ∅ → ( 𝑅 × { 0 } ) = ( ∅ × { 0 } ) )
70 0xp ⊢ ( ∅ × { 0 } ) = ∅
71 69 70 eqtrdi ⊢ ( 𝑅 = ∅ → ( 𝑅 × { 0 } ) = ∅ )
72 71 oveq2d ⊢ ( 𝑅 = ∅ → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) = ( ( 𝑚 + 1 ) Ramsey ∅ ) )
73 simpllr ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → 𝑚 ∈ ℕ0 )
74 peano2nn0 ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ0 )
75 73 74 syl ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( 𝑚 + 1 ) ∈ ℕ0 )
76 ram0 ⊢ ( ( 𝑚 + 1 ) ∈ ℕ0 → ( ( 𝑚 + 1 ) Ramsey ∅ ) = ( 𝑚 + 1 ) )
77 75 76 syl ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( ( 𝑚 + 1 ) Ramsey ∅ ) = ( 𝑚 + 1 ) )
78 72 77 sylan9eqr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) = ( 𝑚 + 1 ) )
79 75 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( 𝑚 + 1 ) ∈ ℕ0 )
80 78 79 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 = ∅ ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) ∈ ℕ0 )
81 75 adantr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → ( 𝑚 + 1 ) ∈ ℕ0 )
82 simp-4l ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → 𝑅 ∈ Fin )
83 simpr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → 𝑅 ≠ ∅ )
84 ramz ⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) = 0 )
85 81 82 83 84 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) = 0 )
86 0nn0 ⊢ 0 ∈ ℕ0
87 85 86 eqeltrdi ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) ∧ 𝑅 ≠ ∅ ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) ∈ ℕ0 )
88 80 87 pm2.61dane ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) ∈ ℕ0 )
89 oveq2 ⊢ ( ℎ = ( 𝑅 × { 0 } ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) = ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) )
90 89 eleq1d ⊢ ( ℎ = ( 𝑅 × { 0 } ) → ( ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ↔ ( ( 𝑚 + 1 ) Ramsey ( 𝑅 × { 0 } ) ) ∈ ℕ0 ) )
91 88 90 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( ℎ = ( 𝑅 × { 0 } ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
92 68 91 sylbid ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ ℎ : 𝑅 ⟶ ℕ0 ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
93 92 expimpd ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
94 93 alrimiv ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 0 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
95 ffn ⊢ ( 𝑓 : 𝑅 ⟶ ℕ0 → 𝑓 Fn 𝑅 )
96 95 ad2antrl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → 𝑓 Fn 𝑅 )
97 ffnfv ⊢ ( 𝑓 : 𝑅 ⟶ ℕ ↔ ( 𝑓 Fn 𝑅 ∧ ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ ) )
98 97 baib ⊢ ( 𝑓 Fn 𝑅 → ( 𝑓 : 𝑅 ⟶ ℕ ↔ ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ ) )
99 96 98 syl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( 𝑓 : 𝑅 ⟶ ℕ ↔ ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ ) )
100 simplr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → 𝑚 ∈ ℕ0 )
101 100 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → 𝑚 ∈ ℕ0 )
102 101 74 syl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( 𝑚 + 1 ) ∈ ℕ0 )
103 simp-4l ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → 𝑅 ∈ Fin )
104 simprr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → 𝑓 : 𝑅 ⟶ ℕ )
105 nnssnn0 ⊢ ℕ ⊆ ℕ0
106 fss ⊢ ( ( 𝑓 : 𝑅 ⟶ ℕ ∧ ℕ ⊆ ℕ0 ) → 𝑓 : 𝑅 ⟶ ℕ0 )
107 104 105 106 sylancl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → 𝑓 : 𝑅 ⟶ ℕ0 )
108 101 nn0cnd ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → 𝑚 ∈ ℂ )
109 ax-1cn ⊢ 1 ∈ ℂ
110 pncan ⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
111 108 109 110 sylancl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
112 111 oveq1d ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) = ( 𝑚 Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) )
113 oveq2 ⊢ ( 𝑔 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( 𝑚 Ramsey 𝑔 ) = ( 𝑚 Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) )
114 113 eleq1d ⊢ ( 𝑔 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) → ( ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ↔ ( 𝑚 Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∈ ℕ0 ) )
115 simprl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 )
116 115 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 )
117 103 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑅 ∈ Fin )
118 117 mptexd ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ∈ V )
119 simpllr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
120 104 ffvelcdmda ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ )
121 nnm1nn0 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( ( 𝑓 ‘ 𝑥 ) − 1 ) ∈ ℕ0 )
122 120 121 syl ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) − 1 ) ∈ ℕ0 )
123 122 adantr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑦 ∈ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) − 1 ) ∈ ℕ0 )
124 107 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑓 : 𝑅 ⟶ ℕ0 )
125 124 ffvelcdmda ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑦 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑦 ) ∈ ℕ0 )
126 123 125 ifcld ⊢ ( ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑦 ∈ 𝑅 ) → if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ∈ ℕ0 )
127 126 fmpttd ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 )
128 simplrr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑓 : 𝑅 ⟶ ℕ )
129 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝑅 )
130 ffvelcdm ⊢ ( ( 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑘 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℕ )
131 130 3ad2antl2 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℕ )
132 131 nncnd ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑘 ) ∈ ℂ )
133 132 subid1d ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → ( ( 𝑓 ‘ 𝑘 ) − 0 ) = ( 𝑓 ‘ 𝑘 ) )
134 133 ifeq2d ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑘 ) − 1 ) , ( ( 𝑓 ‘ 𝑘 ) − 0 ) ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑘 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
135 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
136 135 adantl ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) ∧ 𝑘 = 𝑥 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
137 136 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) ∧ 𝑘 = 𝑥 ) → ( ( 𝑓 ‘ 𝑘 ) − 1 ) = ( ( 𝑓 ‘ 𝑥 ) − 1 ) )
138 137 ifeq1da ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑘 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
139 134 138 eqtr2d ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑘 ) − 1 ) , ( ( 𝑓 ‘ 𝑘 ) − 0 ) ) )
140 ovif2 ⊢ ( ( 𝑓 ‘ 𝑘 ) − if ( 𝑘 = 𝑥 , 1 , 0 ) ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑘 ) − 1 ) , ( ( 𝑓 ‘ 𝑘 ) − 0 ) )
141 139 140 eqtr4di ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 𝑘 ) − if ( 𝑘 = 𝑥 , 1 , 0 ) ) )
142 141 sumeq2dv ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = Σ 𝑘 ∈ 𝑅 ( ( 𝑓 ‘ 𝑘 ) − if ( 𝑘 = 𝑥 , 1 , 0 ) ) )
143 simp1 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → 𝑅 ∈ Fin )
144 0cn ⊢ 0 ∈ ℂ
145 109 144 ifcli ⊢ if ( 𝑘 = 𝑥 , 1 , 0 ) ∈ ℂ
146 145 a1i ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) ∧ 𝑘 ∈ 𝑅 ) → if ( 𝑘 = 𝑥 , 1 , 0 ) ∈ ℂ )
147 143 132 146 fsumsub ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 ( ( 𝑓 ‘ 𝑘 ) − if ( 𝑘 = 𝑥 , 1 , 0 ) ) = ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , 1 , 0 ) ) )
148 elsng ⊢ ( 𝑘 ∈ 𝑅 → ( 𝑘 ∈ { 𝑥 } ↔ 𝑘 = 𝑥 ) )
149 148 ifbid ⊢ ( 𝑘 ∈ 𝑅 → if ( 𝑘 ∈ { 𝑥 } , 1 , 0 ) = if ( 𝑘 = 𝑥 , 1 , 0 ) )
150 149 sumeq2i ⊢ Σ 𝑘 ∈ 𝑅 if ( 𝑘 ∈ { 𝑥 } , 1 , 0 ) = Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , 1 , 0 )
151 simp3 ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ 𝑅 )
152 151 snssd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → { 𝑥 } ⊆ 𝑅 )
153 sumhash ⊢ ( ( 𝑅 ∈ Fin ∧ { 𝑥 } ⊆ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 ∈ { 𝑥 } , 1 , 0 ) = ( ♯ ‘ { 𝑥 } ) )
154 143 152 153 syl2anc ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 ∈ { 𝑥 } , 1 , 0 ) = ( ♯ ‘ { 𝑥 } ) )
155 hashsng ⊢ ( 𝑥 ∈ 𝑅 → ( ♯ ‘ { 𝑥 } ) = 1 )
156 151 155 syl ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → ( ♯ ‘ { 𝑥 } ) = 1 )
157 154 156 eqtrd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 ∈ { 𝑥 } , 1 , 0 ) = 1 )
158 150 157 eqtr3id ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , 1 , 0 ) = 1 )
159 158 oveq2d ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , 1 , 0 ) ) = ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − 1 ) )
160 142 147 159 3eqtrd ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − 1 ) )
161 117 128 129 160 syl3anc ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − 1 ) )
162 simplrl ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) )
163 162 oveq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) − 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
164 simplrr ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
165 164 ad2antrr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑛 ∈ ℕ0 )
166 165 nn0cnd ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → 𝑛 ∈ ℂ )
167 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
168 166 109 167 sylancl ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
169 161 163 168 3eqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 )
170 127 169 jca ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 ) )
171 feq1 ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ℎ : 𝑅 ⟶ ℕ0 ↔ ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 ) )
172 fveq1 ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ℎ ‘ 𝑘 ) = ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ‘ 𝑘 ) )
173 equequ1 ⊢ ( 𝑦 = 𝑘 → ( 𝑦 = 𝑥 ↔ 𝑘 = 𝑥 ) )
174 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑘 ) )
175 173 174 ifbieq2d ⊢ ( 𝑦 = 𝑘 → if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
176 eqid ⊢ ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) )
177 ovex ⊢ ( ( 𝑓 ‘ 𝑥 ) − 1 ) ∈ V
178 fvex ⊢ ( 𝑓 ‘ 𝑘 ) ∈ V
179 177 178 ifex ⊢ if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) ∈ V
180 175 176 179 fvmpt ⊢ ( 𝑘 ∈ 𝑅 → ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
181 172 180 sylan9eq ⊢ ( ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → ( ℎ ‘ 𝑘 ) = if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
182 181 sumeq2dv ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) )
183 182 eqeq1d ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ↔ Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 ) )
184 171 183 anbi12d ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) ↔ ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 ) ) )
185 oveq2 ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) = ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) )
186 185 eleq1d ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ↔ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℕ0 ) )
187 184 186 imbi12d ⊢ ( ℎ = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℕ0 ) ) )
188 187 spcgv ⊢ ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ∈ V → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 if ( 𝑘 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑘 ) ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℕ0 ) ) )
189 118 119 170 188 syl3c ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ∈ ℕ0 )
190 189 fmpttd ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) : 𝑅 ⟶ ℕ0 )
191 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑅 ∈ Fin ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ∈ ( ℕ0 ↑m 𝑅 ) ↔ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) : 𝑅 ⟶ ℕ0 ) )
192 1 103 191 sylancr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ∈ ( ℕ0 ↑m 𝑅 ) ↔ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) : 𝑅 ⟶ ℕ0 ) )
193 190 192 mpbird ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ∈ ( ℕ0 ↑m 𝑅 ) )
194 114 116 193 rspcdva ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( 𝑚 Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∈ ℕ0 )
195 112 194 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∈ ℕ0 )
196 peano2nn0 ⊢ ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) ∈ ℕ0 → ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) + 1 ) ∈ ℕ0 )
197 195 196 syl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) + 1 ) ∈ ℕ0 )
198 nn0p1nn ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ )
199 100 198 syl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( 𝑚 + 1 ) ∈ ℕ )
200 199 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( 𝑚 + 1 ) ∈ ℕ )
201 equequ1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 = 𝑥 ↔ 𝑤 = 𝑥 ) )
202 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑤 ) )
203 201 202 ifbieq2d ⊢ ( 𝑦 = 𝑤 → if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) = if ( 𝑤 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) )
204 203 cbvmptv ⊢ ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) = ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) )
205 eqeq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑤 = 𝑥 ↔ 𝑤 = 𝑧 ) )
206 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑧 ) )
207 206 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) − 1 ) = ( ( 𝑓 ‘ 𝑧 ) − 1 ) )
208 205 207 ifbieq1d ⊢ ( 𝑥 = 𝑧 → if ( 𝑤 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) = if ( 𝑤 = 𝑧 , ( ( 𝑓 ‘ 𝑧 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) )
209 208 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑧 , ( ( 𝑓 ‘ 𝑧 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) ) )
210 204 209 eqtrid ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) = ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑧 , ( ( 𝑓 ‘ 𝑧 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) ) )
211 210 oveq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) = ( ( 𝑚 + 1 ) Ramsey ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑧 , ( ( 𝑓 ‘ 𝑧 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) ) ) )
212 211 cbvmptv ⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) = ( 𝑧 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑤 ∈ 𝑅 ↦ if ( 𝑤 = 𝑧 , ( ( 𝑓 ‘ 𝑧 ) − 1 ) , ( 𝑓 ‘ 𝑤 ) ) ) ) )
213 200 103 104 212 190 195 ramub1 ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ≤ ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) + 1 ) )
214 ramubcl ⊢ ( ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ0 ) ∧ ( ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) + 1 ) ∈ ℕ0 ∧ ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ≤ ( ( ( ( 𝑚 + 1 ) − 1 ) Ramsey ( 𝑥 ∈ 𝑅 ↦ ( ( 𝑚 + 1 ) Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝑓 ‘ 𝑥 ) − 1 ) , ( 𝑓 ‘ 𝑦 ) ) ) ) ) ) + 1 ) ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 )
215 102 103 107 197 213 214 syl32anc ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ∧ 𝑓 : 𝑅 ⟶ ℕ ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 )
216 215 expr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( 𝑓 : 𝑅 ⟶ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
217 216 adantrl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( 𝑓 : 𝑅 ⟶ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
218 99 217 sylbird ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
219 rexnal ⊢ ( ∃ 𝑥 ∈ 𝑅 ¬ ( 𝑓 ‘ 𝑥 ) ∈ ℕ ↔ ¬ ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ )
220 simprl ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → 𝑓 : 𝑅 ⟶ ℕ0 )
221 220 ffvelcdmda ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ 𝑥 ∈ 𝑅 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 )
222 elnn0 ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ0 ↔ ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) )
223 221 222 sylib ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ℕ ∨ ( 𝑓 ‘ 𝑥 ) = 0 ) )
224 223 ord ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ¬ ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( 𝑓 ‘ 𝑥 ) = 0 ) )
225 199 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( 𝑚 + 1 ) ∈ ℕ )
226 simp-4l ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → 𝑅 ∈ Fin )
227 225 226 220 3jca ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( ( 𝑚 + 1 ) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ0 ) )
228 ramz2 ⊢ ( ( ( ( 𝑚 + 1 ) ∈ ℕ ∧ 𝑅 ∈ Fin ∧ 𝑓 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑥 ∈ 𝑅 ∧ ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) = 0 )
229 227 228 sylan ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) = 0 )
230 229 86 eqeltrdi ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ ( 𝑓 ‘ 𝑥 ) = 0 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 )
231 230 expr ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) = 0 → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
232 224 231 syld ⊢ ( ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) ∧ 𝑥 ∈ 𝑅 ) → ( ¬ ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
233 232 rexlimdva ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( ∃ 𝑥 ∈ 𝑅 ¬ ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
234 219 233 biimtrrid ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( ¬ ∀ 𝑥 ∈ 𝑅 ( 𝑓 ‘ 𝑥 ) ∈ ℕ → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
235 218 234 pm2.61d ⊢ ( ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) ∧ ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ∧ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 )
236 235 exp31 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ( ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
237 236 alrimdv ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ∀ 𝑓 ( ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
238 feq1 ⊢ ( ℎ = 𝑓 → ( ℎ : 𝑅 ⟶ ℕ0 ↔ 𝑓 : 𝑅 ⟶ ℕ0 ) )
239 fveq1 ⊢ ( ℎ = 𝑓 → ( ℎ ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
240 239 sumeq2sdv ⊢ ( ℎ = 𝑓 → Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) )
241 240 eqeq1d ⊢ ( ℎ = 𝑓 → ( Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ↔ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) )
242 238 241 anbi12d ⊢ ( ℎ = 𝑓 → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ↔ ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) ) )
243 oveq2 ⊢ ( ℎ = 𝑓 → ( ( 𝑚 + 1 ) Ramsey ℎ ) = ( ( 𝑚 + 1 ) Ramsey 𝑓 ) )
244 243 eleq1d ⊢ ( ℎ = 𝑓 → ( ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ↔ ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
245 242 244 imbi12d ⊢ ( ℎ = 𝑓 → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
246 245 cbvalvw ⊢ ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ∀ 𝑓 ( ( 𝑓 : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
247 237 246 imbitrrdi ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
248 247 anassrs ⊢ ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
249 248 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
250 249 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = 𝑛 ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) → ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = ( 𝑛 + 1 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) ) )
251 36 41 46 51 94 250 nn0ind ⊢ ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ∈ ℕ0 → ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
252 251 com12 ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) → ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ∈ ℕ0 → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
253 252 adantrl ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → ( Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ∈ ℕ0 → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ) )
254 31 253 mpd ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) )
255 240 biantrud ⊢ ( ℎ = 𝑓 → ( ℎ : 𝑅 ⟶ ℕ0 ↔ ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) ) )
256 255 238 bitr3d ⊢ ( ℎ = 𝑓 → ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) ↔ 𝑓 : 𝑅 ⟶ ℕ0 ) )
257 256 244 imbi12d ⊢ ( ℎ = 𝑓 → ( ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) ↔ ( 𝑓 : 𝑅 ⟶ ℕ0 → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
258 257 spvv ⊢ ( ∀ ℎ ( ( ℎ : 𝑅 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑅 ( ℎ ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑅 ( 𝑓 ‘ 𝑘 ) ) → ( ( 𝑚 + 1 ) Ramsey ℎ ) ∈ ℕ0 ) → ( 𝑓 : 𝑅 ⟶ ℕ0 → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
259 254 29 258 sylc ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ∧ ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 ) ) → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 )
260 259 expr ⊢ ( ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ) → ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 → ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
261 260 ralrimdva ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) → ( ∀ 𝑔 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑔 ) ∈ ℕ0 → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
262 27 261 biimtrid ⊢ ( ( 𝑅 ∈ Fin ∧ 𝑚 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) )
263 262 expcom ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑅 ∈ Fin → ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
264 263 a2d ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑚 Ramsey 𝑓 ) ∈ ℕ0 ) → ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( ( 𝑚 + 1 ) Ramsey 𝑓 ) ∈ ℕ0 ) ) )
265 8 12 16 20 24 264 nn0ind ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑅 ∈ Fin → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 ) )
266 265 imp ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ) → ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 )
267 oveq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑀 Ramsey 𝑓 ) = ( 𝑀 Ramsey 𝐹 ) )
268 267 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 ↔ ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ) )
269 268 rspccv ⊢ ( ∀ 𝑓 ∈ ( ℕ0 ↑m 𝑅 ) ( 𝑀 Ramsey 𝑓 ) ∈ ℕ0 → ( 𝐹 ∈ ( ℕ0 ↑m 𝑅 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ) )
270 266 269 syl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ) → ( 𝐹 ∈ ( ℕ0 ↑m 𝑅 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ) )
271 4 270 sylbird ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ) → ( 𝐹 : 𝑅 ⟶ ℕ0 → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ) )
272 271 3impia ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )