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

Theorem ramcl 13076
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 9971 . . . 4  |-  NN0  e.  _V
2 simpr 447 . . . 4  |-  ( ( M  e.  NN0  /\  R  e.  Fin )  ->  R  e.  Fin )
3 elmapg 6785 . . . 4  |-  ( ( NN0  e.  _V  /\  R  e.  Fin )  ->  ( F  e.  ( NN0  ^m  R )  <-> 
F : R --> NN0 )
)
41, 2, 3sylancr 644 . . 3  |-  ( ( M  e.  NN0  /\  R  e.  Fin )  ->  ( F  e.  ( NN0  ^m  R )  <-> 
F : R --> NN0 )
)
5 oveq1 5865 . . . . . . . . 9  |-  ( x  =  0  ->  (
x Ramsey  f )  =  ( 0 Ramsey  f ) )
65eleq1d 2349 . . . . . . . 8  |-  ( x  =  0  ->  (
( x Ramsey  f )  e.  NN0  <->  ( 0 Ramsey  f
)  e.  NN0 )
)
76ralbidv 2563 . . . . . . 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 307 . . . . . 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 5865 . . . . . . . . 9  |-  ( x  =  m  ->  (
x Ramsey  f )  =  ( m Ramsey  f ) )
109eleq1d 2349 . . . . . . . 8  |-  ( x  =  m  ->  (
( x Ramsey  f )  e.  NN0  <->  ( m Ramsey  f
)  e.  NN0 )
)
1110ralbidv 2563 . . . . . . 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 307 . . . . . 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 5865 . . . . . . . . 9  |-  ( x  =  ( m  + 
1 )  ->  (
x Ramsey  f )  =  ( ( m  +  1 ) Ramsey  f ) )
1413eleq1d 2349 . . . . . . . 8  |-  ( x  =  ( m  + 
1 )  ->  (
( x Ramsey  f )  e.  NN0  <->  ( ( m  +  1 ) Ramsey  f
)  e.  NN0 )
)
1514ralbidv 2563 . . . . . . 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 307 . . . . . 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 5865 . . . . . . . . 9  |-  ( x  =  M  ->  (
x Ramsey  f )  =  ( M Ramsey  f ) )
1817eleq1d 2349 . . . . . . . 8  |-  ( x  =  M  ->  (
( x Ramsey  f )  e.  NN0  <->  ( M Ramsey  f
)  e.  NN0 )
)
1918ralbidv 2563 . . . . . . 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 307 . . . . . 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 6792 . . . . . . . 8  |-  ( f  e.  ( NN0  ^m  R )  ->  f : R --> NN0 )
22 0ramcl 13070 . . . . . . . 8  |-  ( ( R  e.  Fin  /\  f : R --> NN0 )  ->  ( 0 Ramsey  f )  e.  NN0 )
2321, 22sylan2 460 . . . . . . 7  |-  ( ( R  e.  Fin  /\  f  e.  ( NN0  ^m  R ) )  -> 
( 0 Ramsey  f )  e.  NN0 )
2423ralrimiva 2626 . . . . . 6  |-  ( R  e.  Fin  ->  A. f  e.  ( NN0  ^m  R
) ( 0 Ramsey  f
)  e.  NN0 )
25 oveq2 5866 . . . . . . . . . . 11  |-  ( f  =  g  ->  (
m Ramsey  f )  =  ( m Ramsey  g ) )
2625eleq1d 2349 . . . . . . . . . 10  |-  ( f  =  g  ->  (
( m Ramsey  f )  e.  NN0  <->  ( m Ramsey  g
)  e.  NN0 )
)
2726cbvralv 2764 . . . . . . . . 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 730 . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . 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 )
30 ffvelrn 5663 . . . . . . . . . . . . . . 15  |-  ( ( f : R --> NN0  /\  k  e.  R )  ->  ( f `  k
)  e.  NN0 )
3129, 30sylan 457 . . . . . . . . . . . . . 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 )
3228, 31fsumnn0cl 12209 . . . . . . . . . . . . 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 )
33 eqeq2 2292 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  0  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  0 ) )
3433anbi2d 684 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  0  ->  (
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  x )  <-> 
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  0 ) ) )
3534imbi1d 308 . . . . . . . . . . . . . . . . . 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 ) ) )
3635albidv 1611 . . . . . . . . . . . . . . . . 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 ) ) )
3736imbi2d 307 . . . . . . . . . . . . . . . 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 ) ) ) )
38 eqeq2 2292 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  n  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  n ) )
3938anbi2d 684 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  n  ->  (
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  x )  <-> 
( h : R --> NN0  /\  sum_ k  e.  R  ( h `  k
)  =  n ) ) )
4039imbi1d 308 . . . . . . . . . . . . . . . . . 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 ) ) )
4140albidv 1611 . . . . . . . . . . . . . . . . 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 ) ) )
4241imbi2d 307 . . . . . . . . . . . . . . . 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 ) ) ) )
43 eqeq2 2292 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( n  + 
1 )  ->  ( sum_ k  e.  R  ( h `  k )  =  x  <->  sum_ k  e.  R  ( h `  k )  =  ( n  +  1 ) ) )
4443anbi2d 684 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
4544imbi1d 308 . . . . . . . . . . . . . . . . . 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 ) ) )
4645albidv 1611 . . . . . . . . . . . . . . . . 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 ) ) )
4746imbi2d 307 . . . . . . . . . . . . . . . 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 ) ) ) )
48 eqeq2 2292 . . . . . . . . . . . . . . . . . . . 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 ) ) )
4948anbi2d 684 . . . . . . . . . . . . . . . . . . 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 )
) ) )
5049imbi1d 308 . . . . . . . . . . . . . . . . . 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 ) ) )
5150albidv 1611 . . . . . . . . . . . . . . . . 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 ) ) )
5251imbi2d 307 . . . . . . . . . . . . . . . 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 ) ) ) )
53 simplll 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( R  e. 
Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0 )  /\  h : R --> NN0 )  ->  R  e.  Fin )
54 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : R --> NN0  /\  k  e.  R )  ->  ( h `  k
)  e.  NN0 )
5554adantll 694 . . . . . . . . . . . . . . . . . . . . . . 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 )
5655nn0red 10019 . . . . . . . . . . . . . . . . . . . . . 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 )
5755nn0ge0d 10021 . . . . . . . . . . . . . . . . . . . . . 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
) )
5853, 56, 57fsum00 12256 . . . . . . . . . . . . . . . . . . . . 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 ) )
59 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h `
 k )  e. 
_V
6059rgenw 2610 . . . . . . . . . . . . . . . . . . . . . 22  |-  A. k  e.  R  ( h `  k )  e.  _V
61 mpteqb 5614 . . . . . . . . . . . . . . . . . . . . . 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 ) )
6260, 61ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  R  |->  ( h `  k ) )  =  ( k  e.  R  |->  0 )  <->  A. k  e.  R  ( h `  k
)  =  0 )
6358, 62syl6bbr 254 . . . . . . . . . . . . . . . . . . . 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 ) ) )
64 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( R  e. 
Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0 )  /\  h : R --> NN0 )  ->  h : R --> NN0 )
6564feqmptd 5575 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
66 fconstmpt 4732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  X.  { 0 } )  =  ( k  e.  R  |->  0 )
6766a1i 10 . . . . . . . . . . . . . . . . . . . . 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 ) )
6865, 67eqeq12d 2297 . . . . . . . . . . . . . . . . . . . 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 ) ) )
6963, 68bitr4d 247 . . . . . . . . . . . . . . . . . . 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 } ) ) )
70 xpeq1 4703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( R  =  (/)  ->  ( R  X.  { 0 } )  =  ( (/)  X. 
{ 0 } ) )
71 xp0r 4768 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (/)  X. 
{ 0 } )  =  (/)
7270, 71syl6eq 2331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( R  =  (/)  ->  ( R  X.  { 0 } )  =  (/) )
7372oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( R  =  (/)  ->  ( ( m  +  1 ) Ramsey 
( R  X.  {
0 } ) )  =  ( ( m  +  1 ) Ramsey  (/) ) )
74 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( R  e. 
Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0 )  /\  h : R --> NN0 )  ->  m  e.  NN0 )
75 peano2nn0 10004 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  NN0  ->  ( m  +  1 )  e. 
NN0 )
7674, 75syl 15 . . . . . . . . . . . . . . . . . . . . . . . 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 )
77 ram0 13069 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( m  +  1 )  e.  NN0  ->  ( ( m  +  1 ) Ramsey  (/) )  =  ( m  +  1 ) )
7876, 77syl 15 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
7973, 78sylan9eqr 2337 . . . . . . . . . . . . . . . . . . . . . 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 ) )
8076adantr 451 . . . . . . . . . . . . . . . . . . . . . 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 )
8179, 80eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . 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 )
8276adantr 451 . . . . . . . . . . . . . . . . . . . . . . 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 )
83 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R ) ( m Ramsey  g )  e.  NN0 )  ->  R  e.  Fin )
8483ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 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 )
85 simpr 447 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  A. g  e.  ( NN0  ^m  R ) ( m Ramsey 
g )  e.  NN0 )  /\  h : R --> NN0 )  /\  R  =/=  (/) )  ->  R  =/=  (/) )
86 ramz 13072 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( m  +  1 )  e.  NN0  /\  R  e.  Fin  /\  R  =/=  (/) )  ->  (
( m  +  1 ) Ramsey  ( R  X.  { 0 } ) )  =  0 )
8782, 84, 85, 86syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 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 )
88 0nn0 9980 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  NN0
8987, 88syl6eqel 2371 . . . . . . . . . . . . . . . . . . . . 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 )
9081, 89pm2.61dane 2524 . . . . . . . . . . . . . . . . . . . 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 )
91 oveq2 5866 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h  =  ( R  X.  { 0 } )  ->  ( ( m  +  1 ) Ramsey  h
)  =  ( ( m  +  1 ) Ramsey 
( R  X.  {
0 } ) ) )
9291eleq1d 2349 . . . . . . . . . . . . . . . . . . . 20  |-  ( h  =  ( R  X.  { 0 } )  ->  ( ( ( m  +  1 ) Ramsey 
h )  e.  NN0  <->  (
( m  +  1 ) Ramsey  ( R  X.  { 0 } ) )  e.  NN0 )
)
9390, 92syl5ibrcom 213 . . . . . . . . . . . . . . . . . . 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 ) )
9469, 93sylbid 206 . . . . . . . . . . . . . . . . . 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 ) )
9594expimpd 586 . . . . . . . . . . . . . . . . 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 ) )
9695alrimiv 1617 . . . . . . . . . . . . . . . 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 ) )
97 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : R --> NN0  ->  f  Fn  R )
9897ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
99 ffnfv 5685 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f : R --> NN  <->  ( f  Fn  R  /\  A. x  e.  R  ( f `  x )  e.  NN ) )
10099baib 871 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  Fn  R  ->  (
f : R --> NN  <->  A. x  e.  R  ( f `  x )  e.  NN ) )
10198, 100syl 15 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
102 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  ( A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0  /\  n  e.  NN0 ) )  ->  m  e.  NN0 )
103102ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
104103, 75syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
105 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( R  e.  Fin  /\  m  e.  NN0 )  /\  ( A. g  e.  ( NN0  ^m  R
) ( m Ramsey  g
)  e.  NN0  /\  n  e.  NN0 ) )  ->  R  e.  Fin )
106105ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
107 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
108 nnssnn0 9968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  NN  C_  NN0
109 fss 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f : R --> NN  /\  NN  C_  NN0 )  -> 
f : R --> NN0 )
110107, 108, 109sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
111103nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
112 ax-1cn 8795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  CC
113 pncan 9057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
114111, 112, 113sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
115114oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
116106adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
117 mptexg 5745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( R  e.  Fin  ->  (
y  e.  R  |->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) ) )  e.  _V )
118116, 117syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
119 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
120 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f : R --> NN  /\  x  e.  R )  ->  ( f `  x
)  e.  NN )
121107, 120sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
122 nnm1nn0 10005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( f `  x )  e.  NN  ->  (
( f `  x
)  -  1 )  e.  NN0 )
123121, 122syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
124123adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
125110adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
126 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( f : R --> NN0  /\  y  e.  R )  ->  ( f `  y
)  e.  NN0 )
127125, 126sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
128 ifcl 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ( f `  x )  -  1 )  e.  NN0  /\  ( f `  y
)  e.  NN0 )  ->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) )  e.  NN0 )
129124, 127, 128syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
130 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )  =  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )
131129, 130fmptd 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
132 simplrr 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 )  ->  f : R --> NN )
133 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
134 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( f : R --> NN  /\  k  e.  R )  ->  ( f `  k
)  e.  NN )
1351343ad2antl2 1118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( f `  k )  e.  NN )
136135nncnd 9762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( f `  k )  e.  CC )
137136subid1d 9146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  ( (
f `  k )  -  0 )  =  ( f `  k
) )
138137ifeq2d 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
139 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  =  x  ->  (
f `  k )  =  ( f `  x ) )
140139adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( ( R  e. 
Fin  /\  f : R
--> NN  /\  x  e.  R )  /\  k  e.  R )  /\  k  =  x )  ->  (
f `  k )  =  ( f `  x ) )
141140oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ( R  e. 
Fin  /\  f : R
--> NN  /\  x  e.  R )  /\  k  e.  R )  /\  k  =  x )  ->  (
( f `  k
)  -  1 )  =  ( ( f `
 x )  - 
1 ) )
142141ifeq1da 3590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
143138, 142eqtr2d 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( if ( k  =  x ,  1 ,  0 )  =  1  -> 
( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  ( ( f `  k
)  -  1 ) )
145 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( if ( k  =  x ,  1 ,  0 )  =  0  -> 
( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  ( ( f `  k
)  -  0 ) )
146144, 145ifsb 3574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( f `  k )  -  if ( k  =  x ,  1 ,  0 ) )  =  if ( k  =  x ,  ( ( f `  k
)  -  1 ) ,  ( ( f `
 k )  - 
0 ) )
147143, 146syl6eqr 2333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
148147sumeq2dv 12176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
149 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  R  e.  Fin )
150 0cn 8831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  0  e.  CC
151112, 150keepel 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  if ( k  =  x ,  1 ,  0 )  e.  CC
152151a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  /\  k  e.  R
)  ->  if (
k  =  x ,  1 ,  0 )  e.  CC )
153149, 136, 152fsumsub 12250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
154 elsncg 3662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( k  e.  R  ->  (
k  e.  { x } 
<->  k  =  x ) )
155154ifbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( k  e.  R  ->  if ( k  e.  {
x } ,  1 ,  0 )  =  if ( k  =  x ,  1 ,  0 ) )
156155sumeq2i 12172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  sum_ k  e.  R  if (
k  e.  { x } ,  1 , 
0 )  =  sum_ k  e.  R  if ( k  =  x ,  1 ,  0 )
157 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  x  e.  R )
158157snssd 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  { x }  C_  R )
159 sumhash 12944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( R  e.  Fin  /\  { x }  C_  R
)  ->  sum_ k  e.  R  if ( k  e.  { x } ,  1 ,  0 )  =  ( # `  { x } ) )
160149, 158, 159syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  e.  {
x } ,  1 ,  0 )  =  ( # `  {
x } ) )
161 hashsng 11356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  R  ->  ( # `
 { x }
)  =  1 )
162157, 161syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  ->  ( # `  {
x } )  =  1 )
163160, 162eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  e.  {
x } ,  1 ,  0 )  =  1 )
164156, 163syl5eqr 2329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( R  e.  Fin  /\  f : R --> NN  /\  x  e.  R )  -> 
sum_ k  e.  R  if ( k  =  x ,  1 ,  0 )  =  1 )
165164oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
166148, 153, 1653eqtrd 2319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
167116, 132, 133, 166syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
168 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
169168oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
170 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
171170ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
172171nn0cnd 10020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
173 pncan 9057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( n  e.  CC  /\  1  e.  CC )  ->  ( ( n  + 
1 )  -  1 )  =  n )
174172, 112, 173sylancl 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 )  ->  (
( n  +  1 )  -  1 )  =  n )
175167, 169, 1743eqtrd 2319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
176131, 175jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
177 feq1 5375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
178 fveq1 5524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
179 equequ1 1648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  =  k  ->  (
y  =  x  <->  k  =  x ) )
180 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( y  =  k  ->  (
f `  y )  =  ( f `  k ) )
181179, 180ifbieq2d 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( y  =  k  ->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) )  =  if ( k  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 k ) ) )
182 ovex 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( f `  x )  -  1 )  e. 
_V
183 fvex 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( f `
 k )  e. 
_V
184182, 183ifex 3623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  if ( k  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 k ) )  e.  _V
185181, 130, 184fvmpt 5602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( k  e.  R  ->  (
( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `  y
) ) ) `  k )  =  if ( k  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  k ) ) )
186178, 185sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
187186sumeq2dv 12176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
188187eqeq1d 2291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
189177, 188anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
190 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
191190eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
192189, 191imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
193192spcgv 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
194118, 119, 176, 193syl3c 57 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
195 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
196194, 195fmptd 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
197 elmapg 6785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
1981, 106, 197sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
199196, 198mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
200 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
201200ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
202 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
203202eleq1d 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
204203rspcv 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
205199, 201, 204sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
206115, 205eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
207 peano2nn0 10004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
208206, 207syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
209 nn0p1nn 10003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  NN )
210102, 209syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211210ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
212 equequ1 1648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  w  ->  (
y  =  x  <->  w  =  x ) )
213 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  w  ->  (
f `  y )  =  ( f `  w ) )
214212, 213ifbieq2d 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  w  ->  if ( y  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  y ) )  =  if ( w  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 w ) ) )
215214cbvmptv 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  R  |->  if ( y  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 y ) ) )  =  ( w  e.  R  |->  if ( w  =  x ,  ( ( f `  x )  -  1 ) ,  ( f `
 w ) ) )
216 eqeq2 2292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
w  =  x  <->  w  =  z ) )
217 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
218217oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
( f `  x
)  -  1 )  =  ( ( f `
 z )  - 
1 ) )
219 eqidd 2284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  z  ->  (
f `  w )  =  ( f `  w ) )
220216, 218, 219ifbieq12d 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  =  z  ->  if ( w  =  x ,  ( ( f `
 x )  - 
1 ) ,  ( f `  w ) )  =  if ( w  =  z ,  ( ( f `  z )  -  1 ) ,  ( f `
 w ) ) )
221220mpteq2dv 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
222215, 221syl5eq 2327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
223222oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
224223cbvmptv 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
225211, 106, 107, 224, 196, 206ramub1 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
226 ramubcl 13065 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
227104, 106, 110, 208, 225, 226syl32anc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
228227expr 598 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
)
229228adantrl 696 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
230101, 229sylbird 226 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
231 rexnal 2554 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E. x  e.  R  -.  ( f `  x
)  e.  NN  <->  -.  A. x  e.  R  ( f `  x )  e.  NN )
232 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
233 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( f : R --> NN0  /\  x  e.  R )  ->  ( f `  x
)  e.  NN0 )
234232, 233sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
235 elnn0 9967 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( f `  x )  e.  NN0  <->  ( ( f `
 x )  e.  NN  \/  ( f `
 x )  =  0 ) )
236234, 235sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
237236ord 366 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
238210ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
239105ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
240238, 239, 2323jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
241 ramz2 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( m  + 
1 )  e.  NN  /\  R  e.  Fin  /\  f : R --> NN0 )  /\  ( x  e.  R  /\  ( f `  x
)  =  0 ) )  ->  ( (
m  +  1 ) Ramsey 
f )  =  0 )
242240, 241sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
243242, 88syl6eqel 2371 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
244243expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
245237, 244syld 40 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
246245rexlimdva 2667 . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
247231, 246syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
248230, 247pm2.61d 150 . . . . . . . . . . . . . . . . . . . . . 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 )
249248exp31 587 . . . . . . . . . . . . . . . . . . . . 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 )