MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ramcl Structured version   Unicode version

Theorem ramcl 13397
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.)
Assertion
Ref Expression
ramcl  |-  ( ( M  e.  NN0  /\  R  e.  Fin  /\  F : R --> NN0 )  ->  ( M Ramsey  F )  e.  NN0 )

Proof of Theorem ramcl
Dummy variables  f  x  g  h  k  m  n  w  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0ex 10227 . . . 4  |-  NN0  e.  _V
2 simpr 448 . . . 4  |-  ( ( M  e.  NN0  /\  R  e.  Fin )  ->  R  e.  Fin )
3 elmapg 7031 . . . 4  |-  ( ( NN0  e.  _V  /\  R  e.  Fin )  ->  ( F  e.  ( NN0  ^m  R )  <-> 
F : R --> NN0 )
)
41, 2, 3sylancr 645 . . 3  |-  ( ( M  e.  NN0  /\  R  e.  Fin )  ->  ( F  e.  ( NN0  ^m  R )  <-> 
F : R --> NN0 )
)
5 oveq1 6088 . . . . . . . . 9  |-  ( x  =  0  ->  (
x Ramsey  f )  =  ( 0 Ramsey  f ) )
65eleq1d 2502 . . . . . . . 8  |-  ( x  =  0  ->  (
( x Ramsey  f )  e.  NN0  <->  ( 0 Ramsey  f
)  e.  NN0 )
)
76ralbidv 2725 . . . . . . 7  |-  ( x  =  0  ->  ( A. f  e.  ( NN0  ^m  R ) ( x Ramsey  f )  e. 
NN0 
<-> 
A. f  e.  ( NN0  ^m  R ) ( 0 Ramsey  f )  e.  NN0 ) )
87imbi2d 308 . . . . . 6  |-  ( 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 6088 . . . . . . . . 9  |-  ( x  =  m  ->  (
x Ramsey  f )  =  ( m Ramsey  f ) )
109eleq1d 2502 . . . . . . . 8  |-  ( x  =  m  ->  (
( x Ramsey  f )  e.  NN0  <->  ( m Ramsey  f
)  e.  NN0 )
)
1110ralbidv 2725 . . . . . . 7  |-  ( x  =  m  ->  ( A. f  e.  ( NN0  ^m  R ) ( x Ramsey  f )  e. 
NN0 
<-> 
A. f  e.  ( NN0  ^m  R ) ( m Ramsey  f )  e.  NN0 ) )
1211imbi2d 308 . . . . . 6  |-  ( 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 6088 . . . . . . . . 9  |-  ( x  =  ( m  + 
1 )  ->  (
x Ramsey  f )  =  ( ( m  +  1 ) Ramsey  f ) )
1413eleq1d 2502 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( x Ramsey  f )  e.  NN0  <->  ( ( m  +  1 ) Ramsey  f
)  e.  NN0 )
)
1514ralbidv 2725 . . . . . . 7  |-  ( 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 ) )
1615imbi2d 308 . . . . . 6  |-  ( 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 6088 . . . . . . . . 9  |-  ( x  =  M  ->  (
x Ramsey  f )  =  ( M Ramsey  f ) )
1817eleq1d 2502 . . . . . . . 8  |-  ( x  =  M  ->  (
( x Ramsey  f )  e.  NN0  <->  ( M Ramsey  f
)  e.  NN0 )
)
1918ralbidv 2725 . . . . . . 7  |-  ( x  =  M  ->  ( A. f  e.  ( NN0  ^m  R ) ( x Ramsey  f )  e. 
NN0 
<-> 
A. f  e.  ( NN0  ^m  R ) ( M Ramsey  f )  e.  NN0 ) )
2019imbi2d 308 . . . . . 6  |-  ( 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 7038 . . . . . . . 8  |-  ( f  e.  ( NN0  ^m  R )  ->  f : R --> NN0 )
22 0ramcl 13391 . . . . . . . 8  |-  ( ( R  e.  Fin  /\  f : R --> NN0 )  ->  ( 0 Ramsey  f )  e.  NN0 )
2321, 22sylan2 461 . . . . . . 7  |-  ( ( R  e.  Fin  /\  f  e.  ( NN0  ^m  R ) )  -> 
( 0 Ramsey  f )  e.  NN0 )
2423ralrimiva 2789 . . . . . 6  |-  ( R  e.  Fin  ->  A. f  e.  ( NN0  ^m  R
) ( 0 Ramsey  f
)  e.  NN0 )
25 oveq2 6089 . . . . . . . . . . 11  |-  ( f  =  g  ->  (
m Ramsey  f )  =  ( m Ramsey  g ) )
2625eleq1d 2502 . . . . . . . . . 10  |-  ( f  =  g  ->  (
( m Ramsey  f )  e.  NN0  <->  ( m Ramsey  g
)  e.  NN0 )
)
2726cbvralv 2932 . . . . . . . . 9  |-  ( A. f  e.  ( NN0  ^m  R ) ( m Ramsey 
f )  e.  NN0  <->  A. g  e.  ( NN0  ^m  R ) ( m Ramsey 
g )  e.  NN0 )
28 simpll 731 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
2921ad2antrl 709 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
3029ffvelrnda 5870 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
3128, 30fsumnn0cl 12530 . . . . . . . . . . . . 13  |-  ( ( ( 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 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  0  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  0 ) )
3332anbi2d 685 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  x )  <-> 
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  0 ) ) )
3433imbi1d 309 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
3534albidv 1635 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
3635imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( 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 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  n  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  n ) )
3837anbi2d 685 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  n  ->  (
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  x )  <-> 
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  n ) ) )
3938imbi1d 309 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
4039albidv 1635 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
4140imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( 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 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( n  + 
1 )  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  ( n  +  1 ) ) )
4342anbi2d 685 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( n  + 
1 )  ->  (
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  x )  <-> 
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  ( n  +  1 ) ) ) )
4443imbi1d 309 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
4544albidv 1635 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
4645imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( 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 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
4847anbi2d 685 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
) ) )
4948imbi1d 309 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) )
5049albidv 1635 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
5150imbi2d 308 . . . . . . . . . . . . . . . 16  |-  ( 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 735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( R  e. 
Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0 )  /\  h : R --> NN0 )  ->  R  e.  Fin )
53 ffvelrn 5868 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : R --> NN0  /\  k  e.  R )  ->  ( h `  k
)  e.  NN0 )
5453adantll 695 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 )
5554nn0red 10275 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 )
5654nn0ge0d 10277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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
) )
5752, 55, 56fsum00 12577 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 5742 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h `
 k )  e. 
_V
5958rgenw 2773 . . . . . . . . . . . . . . . . . . . . . 22  |-  A. k  e.  R  ( h `  k )  e.  _V
60 mpteqb 5819 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. k  e.  R  (
h `  k )  e.  _V  ->  ( (
k  e.  R  |->  ( h `  k ) )  =  ( k  e.  R  |->  0 )  <->  A. k  e.  R  ( h `  k
)  =  0 ) )
6159, 60ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  R  |->  ( h `  k ) )  =  ( k  e.  R  |->  0 )  <->  A. k  e.  R  ( h `  k
)  =  0 )
6257, 61syl6bbr 255 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 448 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( R  e. 
Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0 )  /\  h : R --> NN0 )  ->  h : R --> NN0 )
6463feqmptd 5779 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 4921 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  X.  { 0 } )  =  ( k  e.  R  |->  0 )
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) )
6764, 66eqeq12d 2450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) )
6862, 67bitr4d 248 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 4892 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( R  =  (/)  ->  ( R  X.  { 0 } )  =  ( (/)  X. 
{ 0 } ) )
70 xp0r 4956 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (/)  X. 
{ 0 } )  =  (/)
7169, 70syl6eq 2484 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  =  (/)  ->  ( R  X.  { 0 } )  =  (/) )
7271oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( R  =  (/)  ->  ( ( m  +  1 ) Ramsey 
( R  X.  {
0 } ) )  =  ( ( m  +  1 ) Ramsey  (/) ) )
73 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 10260 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  NN0  ->  ( m  +  1 )  e. 
NN0 )
7573, 74syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 13390 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( m  +  1 )  e.  NN0  ->  ( ( m  +  1 ) Ramsey  (/) )  =  ( m  +  1 ) )
7775, 76syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) )
7872, 77sylan9eqr 2490 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) )
7975adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 )
8078, 79eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 )
8175adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R ) ( m Ramsey 
g )  e.  NN0 )  /\  h : R --> NN0 )  /\  R  =/=  (/) )  ->  R  =/=  (/) )
84 ramz 13393 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( m  +  1 )  e.  NN0  /\  R  e.  Fin  /\  R  =/=  (/) )  ->  (
( m  +  1 ) Ramsey  ( R  X.  { 0 } ) )  =  0 )
8581, 82, 83, 84syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 10236 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  NN0
8785, 86syl6eqel 2524 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 )
8880, 87pm2.61dane 2682 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 6089 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( R  X.  { 0 } )  ->  ( ( m  +  1 ) Ramsey  h
)  =  ( ( m  +  1 ) Ramsey 
( R  X.  {
0 } ) ) )
9089eleq1d 2502 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  ( R  X.  { 0 } )  ->  ( ( ( m  +  1 ) Ramsey 
h )  e.  NN0  <->  (
( m  +  1 ) Ramsey  ( R  X.  { 0 } ) )  e.  NN0 )
)
9188, 90syl5ibrcom 214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) )
9268, 91sylbid 207 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) )
9392expimpd 587 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) )
9493alrimiv 1641 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 5591 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : R --> NN0  ->  f  Fn  R )
9695ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 5894 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : R --> NN  <->  ( f  Fn  R  /\  A. x  e.  R  ( f `  x )  e.  NN ) )
9897baib 872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  Fn  R  ->  (
f : R --> NN  <->  A. x  e.  R  ( f `  x )  e.  NN ) )
9996, 98syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  ( A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0  /\  n  e.  NN0 ) )  ->  m  e.  NN0 )
101100ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
102101, 74syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 10224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  NN  C_  NN0
106 fss 5599 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f : R --> NN  /\  NN  C_  NN0 )  -> 
f : R --> NN0 )
107104, 105, 106sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
108101nn0cnd 10276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( 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 9048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  CC
110 pncan 9311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
111108, 109, 110sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 )
112111oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 ) ) ) ) ) ) )
113103adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 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 )
114 mptexg 5965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( R  e.  Fin  ->  (
y  e.  R  |->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) ) )  e.  _V )
115113, 114syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 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 )
116 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 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 ) )
117104ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( ( ( 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 )
118 nnm1nn0 10261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( f `  x )  e.  NN  ->  (
( f `  x
)  -  1 )  e.  NN0 )
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( 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 )
120119adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( 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 )
121107adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( 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 )
122121ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( ( 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 )
123 ifcl 3775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( f `  x )  -  1 )  e.  NN0  /\  ( f `  y
)  e.  NN0 )  ->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) )  e.  NN0 )
124120, 122, 123syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( ( 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 )
125 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )  =  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )
126124, 125fmptd 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 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 )
127 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( 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 )
128 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( 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 )
129 ffvelrn 5868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( f : R --> NN  /\  k  e.  R )  ->  ( f `  k
)  e.  NN )
1301293ad2antl2 1120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( f `  k )  e.  NN )
131130nncnd 10016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( f `  k )  e.  CC )
132131subid1d 9400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( (
f `  k )  -  0 )  =  ( f `  k
) )
133132ifeq2d 3754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( 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 ) ) )
134 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  =  x  ->  (
f `  k )  =  ( f `  x ) )
135134adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( R  e. 
Fin  /\  f : R
--> NN  /\  x  e.  R )  /\  k  e.  R )  /\  k  =  x )  ->  (
f `  k )  =  ( f `  x ) )
136135oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( R  e. 
Fin  /\  f : R
--> NN  /\  x  e.  R )  /\  k  e.  R )  /\  k  =  x )  ->  (
( f `  k
)  -  1 )  =  ( ( f `
 x )  - 
1 ) )
137136ifeq1da 3764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( 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 ) ) )
138133, 137eqtr2d 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( 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 ) ) )
139 oveq2 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( if ( k  =  x ,  1 ,  0 )  =  1  -> 
( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  ( ( f `  k
)  -  1 ) )
140 oveq2 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( if ( k  =  x ,  1 ,  0 )  =  0  -> 
( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  ( ( f `  k
)  -  0 ) )
141139, 140ifsb 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  if ( k  =  x ,  ( ( f `  k
)  -  1 ) ,  ( ( f `
 k )  - 
0 ) )
142138, 141syl6eqr 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( 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 ) ) )
143142sumeq2dv 12497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 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 ) ) )
144 simp1 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  R  e.  Fin )
145 0cn 9084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  0  e.  CC
146109, 145keepel 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  if ( k  =  x ,  1 ,  0 )  e.  CC
147146a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  if (
k  =  x ,  1 ,  0 )  e.  CC )
148144, 131, 147fsumsub 12571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 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 ) ) )
149 elsncg 3836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( k  e.  R  ->  (
k  e.  { x } 
<->  k  =  x ) )
150149ifbid 3757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( k  e.  R  ->  if ( k  e.  {
x } ,  1 ,  0 )  =  if ( k  =  x ,  1 ,  0 ) )
151150sumeq2i 12493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  sum_ k  e.  R  if (
k  e.  { x } ,  1 , 
0 )  =  sum_ k  e.  R  if ( k  =  x ,  1 ,  0 )
152 simp3 959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  x  e.  R )
153152snssd 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  { x }  C_  R )
154 sumhash 13265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( R  e.  Fin  /\  { x }  C_  R
)  ->  sum_ k  e.  R  if ( k  e.  { x } ,  1 ,  0 )  =  ( # `  { x } ) )
155144, 153, 154syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  e.  {
x } ,  1 ,  0 )  =  ( # `  {
x } ) )
156 hashsng 11647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  R  ->  ( # `
 { x }
)  =  1 )
157152, 156syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  ( # `  {
x } )  =  1 )
158155, 157eqtrd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  e.  {
x } ,  1 ,  0 )  =  1 )
159151, 158syl5eqr 2482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  =  x ,  1 ,  0 )  =  1 )
160159oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( 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 ) )
161143, 148, 1603eqtrd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 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 ) )
162113, 127, 128, 161syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 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 ) )
163 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( 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 ) )
164163oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 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 ) )
165 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( 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 )
166165ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ( ( ( 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 )
167166nn0cnd 10276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( ( ( 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 )
168 pncan 9311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( n  e.  CC  /\  1  e.  CC )  ->  ( ( n  + 
1 )  -  1 )  =  n )
169167, 109, 168sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( ( 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 )
170162, 164, 1693eqtrd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ( 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 )
171126, 170jca 519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ( 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 ) )
172 feq1 5576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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 )
)
173 fveq1 5727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 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 ) )
174 equequ1 1696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  =  k  ->  (
y  =  x  <->  k  =  x ) )
175 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  =  k  ->  (
f `  y )  =  ( f `  k ) )
176174, 175ifbieq2d 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  =  k  ->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) )  =  if ( k  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 k ) ) )
177 ovex 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( f `  x )  -  1 )  e. 
_V
178 fvex 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f `
 k )  e. 
_V
179177, 178ifex 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  if ( k  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 k ) )  e.  _V
180176, 125, 179fvmpt 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( k  e.  R  ->  (
( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) ) ) `  k )  =  if ( k  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  k ) ) )
181173, 180sylan9eq 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 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
) ) )
182181sumeq2dv 12497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 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 ) ) )
183182eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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 ) )
184172, 183anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 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 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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
) ) ) ) )
186185eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 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 )
)
187184, 186imbi12d 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( 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 ) ) )
188187spcgv 3036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 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 ) ) )
189115, 116, 171, 188syl3c 59 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ( 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 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  R  |->  ( ( m  +  1 ) Ramsey 
( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) ) ) ) )  =  ( x  e.  R  |->  ( ( m  +  1 ) Ramsey 
( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) ) ) ) )
191189, 190fmptd 5893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( 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 )
192 elmapg 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 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 )
)
1931, 103, 192sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( 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 ) )
194191, 193mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 ) )
195 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 )
196195ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 )
197 oveq2 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 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 ) ) ) ) ) ) )
198197eleq1d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) )
199198rspcv 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  R  |->  ( ( m  +  1 ) Ramsey  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x
)  -  1 ) ,  ( f `  y ) ) ) ) )  e.  ( NN0  ^m  R )  ->  ( A. g  e.  ( NN0  ^m  R
) ( 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 )
)
200194, 196, 199sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 )
201112, 200eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
202 peano2nn0 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
203201, 202syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
204 nn0p1nn 10259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  NN )
205100, 204syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  ( A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0  /\  n  e.  NN0 ) )  ->  ( m  + 
1 )  e.  NN )
206205ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
207 equequ1 1696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  w  ->  (
y  =  x  <->  w  =  x ) )
208 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  w  ->  (
f `  y )  =  ( f `  w ) )
209207, 208ifbieq2d 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  w  ->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) )  =  if ( w  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 w ) ) )
210209cbvmptv 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )  =  ( w  e.  R  |->  if ( w  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 w ) ) )
211 eqeq2 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
w  =  x  <->  w  =  z ) )
212 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
213212oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
( f `  x
)  -  1 )  =  ( ( f `
 z )  - 
1 ) )
214 eqidd 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
f `  w )  =  ( f `  w ) )
215211, 213, 214ifbieq12d 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  z  ->  if ( w  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  w ) )  =  if ( w  =  z ,  ( ( f `  z )  -  1 ) ,  ( f `
 w ) ) )
216215mpteq2dv 4296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  =  z  ->  (
w  e.  R  |->  if ( w  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  w ) ) )  =  ( w  e.  R  |->  if ( w  =  z ,  ( ( f `
 z )  - 
1 ) ,  ( f `  w ) ) ) )
217210, 216syl5eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  z  ->  (
y  e.  R  |->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) ) )  =  ( w  e.  R  |->  if ( w  =  z ,  ( ( f `
 z )  - 
1 ) ,  ( f `  w ) ) ) )
218217oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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
) ) ) ) )
219218cbvmptv 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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
) ) ) ) )
220206, 103, 104, 219, 191, 201ramub1 13396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 ) )
221 ramubcl 13386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
222102, 103, 107, 203, 220, 221syl32anc 1192 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 )
223222expr 599 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 )
)
224223adantrl 697 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) )
22599, 224sylbird 227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 ) )
226 rexnal 2716 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. x  e.  R  -.  ( f `  x
)  e.  NN  <->  -.  A. x  e.  R  ( f `  x )  e.  NN )
227 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 )
228227ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( 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 )
229 elnn0 10223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f `  x )  e.  NN0  <->  ( ( f `
 x )  e.  NN  \/  ( f `
 x )  =  0 ) )
230228, 229sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( 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 ) )
231230ord 367 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 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 ) )
232205ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 )
233 simp-4l 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( 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 )
234232, 233, 2273jca 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 ) )
235 ramz2 13392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( m  + 
1 )  e.  NN  /\  R  e.  Fin  /\  f : R --> NN0 )  /\  ( x  e.  R  /\  ( f `  x
)  =  0 ) )  ->  ( (
m  +  1 ) Ramsey 
f )  =  0 )
236234, 235sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( 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 )
237236, 86syl6eqel 2524 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ( 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 )
238237expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 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 ) )
239231, 238syld 42 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( 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 ) )
240239rexlimdva 2830 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) )
241226, 240syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 ) )
242225, 241pm2.61d 152 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 )
243242exp31 588 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) )
244243alrimdv 1643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
245 feq1 5576 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  f  ->  (
h : R --> NN0  <->  f : R
--> NN0 ) )
246 fveq1 5727 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h  =  f  ->  (
h `  k )  =  ( f `  k ) )
247246sumeq2sdv 12498 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h  =  f  ->  sum_ k  e.  R  ( h `  k )  =  sum_ k  e.  R  (
f `  k )
)
248247eqeq1d 2444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  =  f  ->  ( sum_ k  e.  R  ( h `  k )  =  ( n  + 
1 )  <->  sum_ k  e.  R  ( f `