Metamath Proof Explorer


Theorem ramcl

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

Ref Expression
Assertion ramcl
|- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )

Proof

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