# 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( ( ( 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 )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) )`
` |-  ( ( ( ( ( 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 ) ) )`
` |-  ( ( ( 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 )`