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 
|- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )

Proof

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