MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ramcl Structured version   Visualization version   Unicode version
Theorem ramcl 15733
Description: Ramsey's theorem: the Ramsey number is an integer for every finite coloring and set of upper bounds. (Contributed by Mario Carneiro, 23-Apr-2015.)
Assertion
Ref Expression
ramcl |- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )
Proof of Theorem ramcl
Dummy variables f x g h k m n w y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0ex 11298 . . . 4 |- NN0 e. _V
2 simpr 477 . . . 4 |- ( ( M e. NN0 /\ R e. Fin ) -> R e. Fin )
3 elmapg 7870 . . . 4 |- ( ( NN0 e. _V /\ R e. Fin ) -> ( F e. ( NN0 ^m R ) <-> F : R --> NN0 ) )
41, 2, 3sylancr 695 . . 3 |- ( ( M e. NN0 /\ R e. Fin ) -> ( F e. ( NN0 ^m R ) <-> F : R --> NN0 ) )
5 oveq1 6657 . . . . . . . . 9 |- ( x = 0 -> ( x Ramsey f ) = ( 0 Ramsey f ) )
65eleq1d 2686 . . . . . . . 8 |- ( x = 0 -> ( ( x Ramsey f ) e. NN0 <-> ( 0 Ramsey f ) e. NN0 ) )
76ralbidv 2986 . . . . . . 7 |- ( x = 0 -> ( A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 <-> A. f e. ( NN0 ^m R ) ( 0 Ramsey f ) e. NN0 ) )
87imbi2d 330 . . . . . 6 |- ( x = 0 -> ( ( R e. Fin -> A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 ) <-> ( R e. Fin -> A. f e. ( NN0 ^m R ) ( 0 Ramsey f ) e. NN0 ) ) )
9 oveq1 6657 . . . . . . . . 9 |- ( x = m -> ( x Ramsey f ) = ( m Ramsey f ) )
109eleq1d 2686 . . . . . . . 8 |- ( x = m -> ( ( x Ramsey f ) e. NN0 <-> ( m Ramsey f ) e. NN0 ) )
1110ralbidv 2986 . . . . . . 7 |- ( x = m -> ( A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 <-> A. f e. ( NN0 ^m R ) ( m Ramsey f ) e. NN0 ) )
1211imbi2d 330 . . . . . 6 |- ( x = m -> ( ( R e. Fin -> A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 ) <-> ( R e. Fin -> A. f e. ( NN0 ^m R ) ( m Ramsey f ) e. NN0 ) ) )
13 oveq1 6657 . . . . . . . . 9 |- ( x = ( m + 1 ) -> ( x Ramsey f ) = ( ( m + 1 ) Ramsey f ) )
1413eleq1d 2686 . . . . . . . 8 |- ( x = ( m + 1 ) -> ( ( x Ramsey f ) e. NN0 <-> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
1514ralbidv 2986 . . . . . . 7 |- ( x = ( m + 1 ) -> ( A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 <-> A. f e. ( NN0 ^m R ) ( ( m + 1 ) Ramsey f ) e. NN0 ) )
1615imbi2d 330 . . . . . 6 |- ( x = ( m + 1 ) -> ( ( R e. Fin -> A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 ) <-> ( R e. Fin -> A. f e. ( NN0 ^m R ) ( ( m + 1 ) Ramsey f ) e. NN0 ) ) )
17 oveq1 6657 . . . . . . . . 9 |- ( x = M -> ( x Ramsey f ) = ( M Ramsey f ) )
1817eleq1d 2686 . . . . . . . 8 |- ( x = M -> ( ( x Ramsey f ) e. NN0 <-> ( M Ramsey f ) e. NN0 ) )
1918ralbidv 2986 . . . . . . 7 |- ( x = M -> ( A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 <-> A. f e. ( NN0 ^m R ) ( M Ramsey f ) e. NN0 ) )
2019imbi2d 330 . . . . . 6 |- ( x = M -> ( ( R e. Fin -> A. f e. ( NN0 ^m R ) ( x Ramsey f ) e. NN0 ) <-> ( R e. Fin -> A. f e. ( NN0 ^m R ) ( M Ramsey f ) e. NN0 ) ) )
21 elmapi 7879 . . . . . . . 8 |- ( f e. ( NN0 ^m R ) -> f : R --> NN0 )
22 0ramcl 15727 . . . . . . . 8 |- ( ( R e. Fin /\ f : R --> NN0 ) -> ( 0 Ramsey f ) e. NN0 )
2321, 22sylan2 491 . . . . . . 7 |- ( ( R e. Fin /\ f e. ( NN0 ^m R ) ) -> ( 0 Ramsey f ) e. NN0 )
2423ralrimiva 2966 . . . . . 6 |- ( R e. Fin -> A. f e. ( NN0 ^m R ) ( 0 Ramsey f ) e. NN0 )
25 oveq2 6658 . . . . . . . . . . 11 |- ( f = g -> ( m Ramsey f ) = ( m Ramsey g ) )
2625eleq1d 2686 . . . . . . . . . 10 |- ( f = g -> ( ( m Ramsey f ) e. NN0 <-> ( m Ramsey g ) e. NN0 ) )
2726cbvralv 3171 . . . . . . . . 9 |- ( A. f e. ( NN0 ^m R ) ( m Ramsey f ) e. NN0 <-> A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 )
28 simpll 790 . . . . . . . . . . . . . 14 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( f e. ( NN0 ^m R ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) ) -> R e. Fin )
2921ad2antrl 764 . . . . . . . . . . . . . . 15 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( f e. ( NN0 ^m R ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) ) -> f : R --> NN0 )
3029ffvelrnda 6359 . . . . . . . . . . . . . 14 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( f e. ( NN0 ^m R ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) ) /\ k e. R ) -> ( f ` k ) e. NN0 )
3128, 30fsumnn0cl 14467 . . . . . . . . . . . . 13 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( f e. ( NN0 ^m R ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) ) -> sum_ k e. R ( f ` k ) e. NN0 )
32 eqeq2 2633 . . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( sum_ k e. R ( h ` k ) = x <-> sum_ k e. R ( h ` k ) = 0 ) )
3332anbi2d 740 . . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) <-> ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) ) )
3433imbi1d 331 . . . . . . . . . . . . . . . . . 18 |- ( x = 0 -> ( ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
3534albidv 1849 . . . . . . . . . . . . . . . . 17 |- ( x = 0 -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
3635imbi2d 330 . . . . . . . . . . . . . . . 16 |- ( x = 0 -> ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) <-> ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) ) )
37 eqeq2 2633 . . . . . . . . . . . . . . . . . . . 20 |- ( x = n -> ( sum_ k e. R ( h ` k ) = x <-> sum_ k e. R ( h ` k ) = n ) )
3837anbi2d 740 . . . . . . . . . . . . . . . . . . 19 |- ( x = n -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) <-> ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) ) )
3938imbi1d 331 . . . . . . . . . . . . . . . . . 18 |- ( x = n -> ( ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
4039albidv 1849 . . . . . . . . . . . . . . . . 17 |- ( x = n -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
4140imbi2d 330 . . . . . . . . . . . . . . . 16 |- ( x = n -> ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) <-> ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) ) )
42 eqeq2 2633 . . . . . . . . . . . . . . . . . . . 20 |- ( x = ( n + 1 ) -> ( sum_ k e. R ( h ` k ) = x <-> sum_ k e. R ( h ` k ) = ( n + 1 ) ) )
4342anbi2d 740 . . . . . . . . . . . . . . . . . . 19 |- ( x = ( n + 1 ) -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) <-> ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = ( n + 1 ) ) ) )
4443imbi1d 331 . . . . . . . . . . . . . . . . . 18 |- ( x = ( n + 1 ) -> ( ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = ( n + 1 ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
4544albidv 1849 . . . . . . . . . . . . . . . . 17 |- ( x = ( n + 1 ) -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = ( n + 1 ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
4645imbi2d 330 . . . . . . . . . . . . . . . 16 |- ( x = ( n + 1 ) -> ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) <-> ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = ( n + 1 ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) ) )
47 eqeq2 2633 . . . . . . . . . . . . . . . . . . . 20 |- ( x = sum_ k e. R ( f ` k ) -> ( sum_ k e. R ( h ` k ) = x <-> sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) )
4847anbi2d 740 . . . . . . . . . . . . . . . . . . 19 |- ( x = sum_ k e. R ( f ` k ) -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) <-> ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) ) )
4948imbi1d 331 . . . . . . . . . . . . . . . . . 18 |- ( x = sum_ k e. R ( f ` k ) -> ( ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
5049albidv 1849 . . . . . . . . . . . . . . . . 17 |- ( x = sum_ k e. R ( f ` k ) -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
5150imbi2d 330 . . . . . . . . . . . . . . . 16 |- ( x = sum_ k e. R ( f ` k ) -> ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = x ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) <-> ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) ) )
52 simplll 798 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> R e. Fin )
53 ffvelrn 6357 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( h : R --> NN0 /\ k e. R ) -> ( h ` k ) e. NN0 )
5453adantll 750 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ k e. R ) -> ( h ` k ) e. NN0 )
5554nn0red 11352 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ k e. R ) -> ( h ` k ) e. RR )
5654nn0ge0d 11354 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ k e. R ) -> 0 <_ ( h ` k ) )
5752, 55, 56fsum00 14530 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( sum_ k e. R ( h ` k ) = 0 <-> A. k e. R ( h ` k ) = 0 ) )
58 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( h ` k ) e. _V
5958rgenw 2924 . . . . . . . . . . . . . . . . . . . . . 22 |- A. k e. R ( h ` k ) e. _V
60 mpteqb 6299 . . . . . . . . . . . . . . . . . . . . . 22 |- ( A. k e. R ( h ` k ) e. _V -> ( ( k e. R |-> ( h ` k ) ) = ( k e. R |-> 0 ) <-> A. k e. R ( h ` k ) = 0 ) )
6159, 60ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( k e. R |-> ( h ` k ) ) = ( k e. R |-> 0 ) <-> A. k e. R ( h ` k ) = 0 )
6257, 61syl6bbr 278 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( sum_ k e. R ( h ` k ) = 0 <-> ( k e. R |-> ( h ` k ) ) = ( k e. R |-> 0 ) ) )
63 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> h : R --> NN0 )
6463feqmptd 6249 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> h = ( k e. R |-> ( h ` k ) ) )
65 fconstmpt 5163 . . . . . . . . . . . . . . . . . . . . . 22 |- ( R X. { 0 } ) = ( k e. R |-> 0 )
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( R X. { 0 } ) = ( k e. R |-> 0 ) )
6764, 66eqeq12d 2637 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( h = ( R X. { 0 } ) <-> ( k e. R |-> ( h ` k ) ) = ( k e. R |-> 0 ) ) )
6862, 67bitr4d 271 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( sum_ k e. R ( h ` k ) = 0 <-> h = ( R X. { 0 } ) ) )
69 xpeq1 5128 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( R = (/) -> ( R X. { 0 } ) = ( (/) X. { 0 } ) )
70 0xp 5199 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( (/) X. { 0 } ) = (/)
7169, 70syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( R = (/) -> ( R X. { 0 } ) = (/) )
7271oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( R = (/) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) = ( ( m + 1 ) Ramsey (/) ) )
73 simpllr 799 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> m e. NN0 )
74 peano2nn0 11333 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( m e. NN0 -> ( m + 1 ) e. NN0 )
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( m + 1 ) e. NN0 )
76 ram0 15726 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( m + 1 ) e. NN0 -> ( ( m + 1 ) Ramsey (/) ) = ( m + 1 ) )
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( ( m + 1 ) Ramsey (/) ) = ( m + 1 ) )
7872, 77sylan9eqr 2678 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R = (/) ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) = ( m + 1 ) )
7975adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R = (/) ) -> ( m + 1 ) e. NN0 )
8078, 79eqeltrd 2701 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R = (/) ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) e. NN0 )
8175adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R =/= (/) ) -> ( m + 1 ) e. NN0 )
82 simp-4l 806 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R =/= (/) ) -> R e. Fin )
83 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R =/= (/) ) -> R =/= (/) )
84 ramz 15729 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( m + 1 ) e. NN0 /\ R e. Fin /\ R =/= (/) ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) = 0 )
8581, 82, 83, 84syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R =/= (/) ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) = 0 )
86 0nn0 11307 . . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. NN0
8785, 86syl6eqel 2709 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) /\ R =/= (/) ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) e. NN0 )
8880, 87pm2.61dane 2881 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) e. NN0 )
89 oveq2 6658 . . . . . . . . . . . . . . . . . . . . 21 |- ( h = ( R X. { 0 } ) -> ( ( m + 1 ) Ramsey h ) = ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) )
9089eleq1d 2686 . . . . . . . . . . . . . . . . . . . 20 |- ( h = ( R X. { 0 } ) -> ( ( ( m + 1 ) Ramsey h ) e. NN0 <-> ( ( m + 1 ) Ramsey ( R X. { 0 } ) ) e. NN0 ) )
9188, 90syl5ibrcom 237 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( h = ( R X. { 0 } ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) )
9268, 91sylbid 230 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) /\ h : R --> NN0 ) -> ( sum_ k e. R ( h ` k ) = 0 -> ( ( m + 1 ) Ramsey h ) e. NN0 ) )
9392expimpd 629 . . . . . . . . . . . . . . . . 17 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) )
9493alrimiv 1855 . . . . . . . . . . . . . . . 16 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = 0 ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) )
95 ffn 6045 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : R --> NN0 -> f Fn R )
9695ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> f Fn R )
97 ffnfv 6388 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( f : R --> NN <-> ( f Fn R /\ A. x e. R ( f ` x ) e. NN ) )
9897baib 944 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f Fn R -> ( f : R --> NN <-> A. x e. R ( f ` x ) e. NN ) )
9996, 98syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( f : R --> NN <-> A. x e. R ( f ` x ) e. NN ) )
100 simplr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) -> m e. NN0 )
101100ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> m e. NN0 )
102101, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( m + 1 ) e. NN0 )
103 simp-4l 806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> R e. Fin )
104 simprr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> f : R --> NN )
105 nnssnn0 11295 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- NN C_ NN0
106 fss 6056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( f : R --> NN /\ NN C_ NN0 ) -> f : R --> NN0 )
107104, 105, 106sylancl 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> f : R --> NN0 )
108101nn0cnd 11353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> m e. CC )
109 ax-1cn 9994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- 1 e. CC
110 pncan 10287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
111108, 109, 110sylancl 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( m + 1 ) - 1 ) = m )
112111oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) = ( m Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) )
113103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> R e. Fin )
114 mptexg 6484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( R e. Fin -> ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) e. _V )
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) e. _V )
116 simpllr 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) )
117104ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( f ` x ) e. NN )
118 nnm1nn0 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( f ` x ) e. NN -> ( ( f ` x ) - 1 ) e. NN0 )
119117, 118syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( ( f ` x ) - 1 ) e. NN0 )
120119adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) /\ y e. R ) -> ( ( f ` x ) - 1 ) e. NN0 )
121107adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> f : R --> NN0 )
122121ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) /\ y e. R ) -> ( f ` y ) e. NN0 )
123120, 122ifcld 4131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) /\ y e. R ) -> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) e. NN0 )
124 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) )
125123, 124fmptd 6385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 )
126 simplrr 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> f : R --> NN )
127 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> x e. R )
128 ffvelrn 6357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( f : R --> NN /\ k e. R ) -> ( f ` k ) e. NN )
1291283ad2antl2 1224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> ( f ` k ) e. NN )
130129nncnd 11036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> ( f ` k ) e. CC )
131130subid1d 10381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> ( ( f ` k ) - 0 ) = ( f ` k ) )
132131ifeq2d 4105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> if ( k = x , ( ( f ` k ) - 1 ) , ( ( f ` k ) - 0 ) ) = if ( k = x , ( ( f ` k ) - 1 ) , ( f ` k ) ) )
133 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( k = x -> ( f ` k ) = ( f ` x ) )
134133adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) /\ k = x ) -> ( f ` k ) = ( f ` x ) )
135134oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) /\ k = x ) -> ( ( f ` k ) - 1 ) = ( ( f ` x ) - 1 ) )
136135ifeq1da 4116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> if ( k = x , ( ( f ` k ) - 1 ) , ( f ` k ) ) = if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) )
137132, 136eqtr2d 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = if ( k = x , ( ( f ` k ) - 1 ) , ( ( f ` k ) - 0 ) ) )
138 ovif2 6738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f ` k ) - if ( k = x , 1 , 0 ) ) = if ( k = x , ( ( f ` k ) - 1 ) , ( ( f ` k ) - 0 ) )
139137, 138syl6eqr 2674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = ( ( f ` k ) - if ( k = x , 1 , 0 ) ) )
140139sumeq2dv 14433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = sum_ k e. R ( ( f ` k ) - if ( k = x , 1 , 0 ) ) )
141 simp1 1061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> R e. Fin )
142 0cn 10032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- 0 e. CC
143109, 142keepel 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- if ( k = x , 1 , 0 ) e. CC
144143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( R e. Fin /\ f : R --> NN /\ x e. R ) /\ k e. R ) -> if ( k = x , 1 , 0 ) e. CC )
145141, 130, 144fsumsub 14520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R ( ( f ` k ) - if ( k = x , 1 , 0 ) ) = ( sum_ k e. R ( f ` k ) - sum_ k e. R if ( k = x , 1 , 0 ) ) )
146 elsng 4191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( k e. R -> ( k e. { x } <-> k = x ) )
147146ifbid 4108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( k e. R -> if ( k e. { x } , 1 , 0 ) = if ( k = x , 1 , 0 ) )
148147sumeq2i 14429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- sum_ k e. R if ( k e. { x } , 1 , 0 ) = sum_ k e. R if ( k = x , 1 , 0 )
149 simp3 1063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> x e. R )
150149snssd 4340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> { x } C_ R )
151 sumhash 15600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( R e. Fin /\ { x } C_ R ) -> sum_ k e. R if ( k e. { x } , 1 , 0 ) = ( # ` { x } ) )
152141, 150, 151syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R if ( k e. { x } , 1 , 0 ) = ( # ` { x } ) )
153 hashsng 13159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( x e. R -> ( # ` { x } ) = 1 )
154149, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> ( # ` { x } ) = 1 )
155152, 154eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R if ( k e. { x } , 1 , 0 ) = 1 )
156148, 155syl5eqr 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R if ( k = x , 1 , 0 ) = 1 )
157156oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> ( sum_ k e. R ( f ` k ) - sum_ k e. R if ( k = x , 1 , 0 ) ) = ( sum_ k e. R ( f ` k ) - 1 ) )
158140, 145, 1573eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( R e. Fin /\ f : R --> NN /\ x e. R ) -> sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = ( sum_ k e. R ( f ` k ) - 1 ) )
159113, 126, 127, 158syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = ( sum_ k e. R ( f ` k ) - 1 ) )
160 simplrl 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> sum_ k e. R ( f ` k ) = ( n + 1 ) )
161160oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( sum_ k e. R ( f ` k ) - 1 ) = ( ( n + 1 ) - 1 ) )
162 simplrr 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) -> n e. NN0 )
163162ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> n e. NN0 )
164163nn0cnd 11353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> n e. CC )
165 pncan 10287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
166164, 109, 165sylancl 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( ( n + 1 ) - 1 ) = n )
167159, 161, 1663eqtrd 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n )
168125, 167jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 /\ sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n ) )
169 feq1 6026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( h : R --> NN0 <-> ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 ) )
170 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( h ` k ) = ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ` k ) )
171 equequ1 1952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( y = k -> ( y = x <-> k = x ) )
172 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( y = k -> ( f ` y ) = ( f ` k ) )
173171, 172ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( y = k -> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) = if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) )
174 ovex 6678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( f ` x ) - 1 ) e. _V
175 fvex 6201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( f ` k ) e. _V
176174, 175ifex 4156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) e. _V
177173, 124, 176fvmpt 6282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( k e. R -> ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ` k ) = if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) )
178170, 177sylan9eq 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) /\ k e. R ) -> ( h ` k ) = if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) )
179178sumeq2dv 14433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> sum_ k e. R ( h ` k ) = sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) )
180179eqeq1d 2624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( sum_ k e. R ( h ` k ) = n <-> sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n ) )
181169, 180anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) <-> ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 /\ sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n ) ) )
182 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( ( m + 1 ) Ramsey h ) = ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) )
183182eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( ( ( m + 1 ) Ramsey h ) e. NN0 <-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) e. NN0 ) )
184181, 183imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( h = ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) -> ( ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) <-> ( ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 /\ sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n ) -> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) e. NN0 ) ) )
185184spcgv 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) e. _V -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) -> ( ( ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) : R --> NN0 /\ sum_ k e. R if ( k = x , ( ( f ` x ) - 1 ) , ( f ` k ) ) = n ) -> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) e. NN0 ) ) )
186115, 116, 168, 185syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) /\ x e. R ) -> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) e. NN0 )
187 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) = ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) )
188186, 187fmptd 6385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) : R --> NN0 )
189 elmapg 7870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( NN0 e. _V /\ R e. Fin ) -> ( ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) e. ( NN0 ^m R ) <-> ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) : R --> NN0 ) )
1901, 103, 189sylancr 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) e. ( NN0 ^m R ) <-> ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) : R --> NN0 ) )
191188, 190mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) e. ( NN0 ^m R ) )
192 simprl 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) -> A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 )
193192ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 )
194 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( g = ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) -> ( m Ramsey g ) = ( m Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) )
195194eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g = ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) -> ( ( m Ramsey g ) e. NN0 <-> ( m Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) e. NN0 ) )
196195rspcv 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) e. ( NN0 ^m R ) -> ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 -> ( m Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) e. NN0 ) )
197191, 193, 196sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( m Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) e. NN0 )
198112, 197eqeltrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) e. NN0 )
199 peano2nn0 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) e. NN0 -> ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) + 1 ) e. NN0 )
200198, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) + 1 ) e. NN0 )
201 nn0p1nn 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( m e. NN0 -> ( m + 1 ) e. NN )
202100, 201syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) -> ( m + 1 ) e. NN )
203202ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( m + 1 ) e. NN )
204 equequ1 1952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( y = w -> ( y = x <-> w = x ) )
205 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( y = w -> ( f ` y ) = ( f ` w ) )
206204, 205ifbieq2d 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y = w -> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) = if ( w = x , ( ( f ` x ) - 1 ) , ( f ` w ) ) )
207206cbvmptv 4750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) = ( w e. R |-> if ( w = x , ( ( f ` x ) - 1 ) , ( f ` w ) ) )
208 eqeq2 2633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( x = z -> ( w = x <-> w = z ) )
209 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x = z -> ( f ` x ) = ( f ` z ) )
210209oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( x = z -> ( ( f ` x ) - 1 ) = ( ( f ` z ) - 1 ) )
211208, 210ifbieq1d 4109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x = z -> if ( w = x , ( ( f ` x ) - 1 ) , ( f ` w ) ) = if ( w = z , ( ( f ` z ) - 1 ) , ( f ` w ) ) )
212211mpteq2dv 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x = z -> ( w e. R |-> if ( w = x , ( ( f ` x ) - 1 ) , ( f ` w ) ) ) = ( w e. R |-> if ( w = z , ( ( f ` z ) - 1 ) , ( f ` w ) ) ) )
213207, 212syl5eq 2668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x = z -> ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) = ( w e. R |-> if ( w = z , ( ( f ` z ) - 1 ) , ( f ` w ) ) ) )
214213oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x = z -> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) = ( ( m + 1 ) Ramsey ( w e. R |-> if ( w = z , ( ( f ` z ) - 1 ) , ( f ` w ) ) ) ) )
215214cbvmptv 4750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) = ( z e. R |-> ( ( m + 1 ) Ramsey ( w e. R |-> if ( w = z , ( ( f ` z ) - 1 ) , ( f ` w ) ) ) ) )
216203, 103, 104, 215, 188, 198ramub1 15732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( m + 1 ) Ramsey f ) <_ ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) + 1 ) )
217 ramubcl 15722 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( m + 1 ) e. NN0 /\ R e. Fin /\ f : R --> NN0 ) /\ ( ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) + 1 ) e. NN0 /\ ( ( m + 1 ) Ramsey f ) <_ ( ( ( ( m + 1 ) - 1 ) Ramsey ( x e. R |-> ( ( m + 1 ) Ramsey ( y e. R |-> if ( y = x , ( ( f ` x ) - 1 ) , ( f ` y ) ) ) ) ) ) + 1 ) ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 )
218102, 103, 107, 200, 216, 217syl32anc 1334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( sum_ k e. R ( f ` k ) = ( n + 1 ) /\ f : R --> NN ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 )
219218expr 643 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) -> ( f : R --> NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
220219adantrl 752 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( f : R --> NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
22199, 220sylbird 250 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( A. x e. R ( f ` x ) e. NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
222 rexnal 2995 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( E. x e. R -. ( f ` x ) e. NN <-> -. A. x e. R ( f ` x ) e. NN )
223 simprl 794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> f : R --> NN0 )
224223ffvelrnda 6359 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ x e. R ) -> ( f ` x ) e. NN0 )
225 elnn0 11294 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( f ` x ) e. NN0 <-> ( ( f ` x ) e. NN \/ ( f ` x ) = 0 ) )
226224, 225sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ x e. R ) -> ( ( f ` x ) e. NN \/ ( f ` x ) = 0 ) )
227226ord 392 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ x e. R ) -> ( -. ( f ` x ) e. NN -> ( f ` x ) = 0 ) )
228202ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( m + 1 ) e. NN )
229 simp-4l 806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> R e. Fin )
230228, 229, 2233jca 1242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( ( m + 1 ) e. NN /\ R e. Fin /\ f : R --> NN0 ) )
231 ramz2 15728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( m + 1 ) e. NN /\ R e. Fin /\ f : R --> NN0 ) /\ ( x e. R /\ ( f ` x ) = 0 ) ) -> ( ( m + 1 ) Ramsey f ) = 0 )
232230, 231sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ ( x e. R /\ ( f ` x ) = 0 ) ) -> ( ( m + 1 ) Ramsey f ) = 0 )
233232, 86syl6eqel 2709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ ( x e. R /\ ( f ` x ) = 0 ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 )
234233expr 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ x e. R ) -> ( ( f ` x ) = 0 -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
235227, 234syld 47 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) /\ x e. R ) -> ( -. ( f ` x ) e. NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
236235rexlimdva 3031 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( E. x e. R -. ( f ` x ) e. NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
237222, 236syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( -. A. x e. R ( f ` x ) e. NN -> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
238221, 237pm2.61d 170 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) /\ A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) /\ ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 )
239238exp31 630 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) -> ( ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 ) ) )
240239alrimdv 1857 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 /\ n e. NN0 ) ) -> ( A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = n ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) -> A. f ( ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) -> ( ( m + 1 ) Ramsey f ) e. NN0 ) ) )
241 feq1 6026 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( h = f -> ( h : R --> NN0 <-> f : R --> NN0 ) )
242 fveq1 6190 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( h = f -> ( h ` k ) = ( f ` k ) )
243242sumeq2sdv 14435 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( h = f -> sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) )
244243eqeq1d 2624 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( h = f -> ( sum_ k e. R ( h ` k ) = ( n + 1 ) <-> sum_ k e. R ( f ` k ) = ( n + 1 ) ) )
245241, 244anbi12d 747 . . . . . . . . . . . . . . . . . . . . . 22 |- ( h = f -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = ( n + 1 ) ) <-> ( f : R --> NN0 /\ sum_ k e. R ( f ` k ) = ( n + 1 ) ) ) )
246 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( h = f -> ( ( m + 1 ) Ramsey h ) = ( ( m + 1 ) Ramsey f ) )
247246eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . 22 |- ( h = f -> ( ( ( m + 1 ) Ramsey h ) e. NN0 <-> ( ( m + 1 ) Ramsey f ) e. NN0 ) )
248245, 247imbi12d 334 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
249248cbvalv 2273 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) )
250240, 249syl6ibr 242 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( A. g e. ( NN0 ^m R ) ( m Ramsey 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 ) ) )
251250anassrs 680 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( R e. Fin /\ m e. NN0 ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey 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 ) ) )
252251expcom 451 . . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) )
253252a2d 29 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
25436, 41, 46, 51, 94, 253nn0ind 11472 . . . . . . . . . . . . . . 15 |- ( 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 ) ) )
255254com12 32 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
256255adantrl 752 . . . . . . . . . . . . 13 |- ( ( ( R e. Fin /\ m e. NN0 ) /\ ( f e. ( NN0 ^m R ) /\ A. g e. ( NN0 ^m R ) ( m Ramsey g ) e. NN0 ) ) -> ( sum_ k e. R ( f ` k ) e. NN0 -> A. h ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) -> ( ( m + 1 ) Ramsey h ) e. NN0 ) ) )
25731, 256mpd 15 . . . . . . . . . . . 12 |- ( ( ( 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 ) )
258243biantrud 528 . . . . . . . . . . . . . . 15 |- ( h = f -> ( h : R --> NN0 <-> ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) ) )
259258, 241bitr3d 270 . . . . . . . . . . . . . 14 |- ( h = f -> ( ( h : R --> NN0 /\ sum_ k e. R ( h ` k ) = sum_ k e. R ( f ` k ) ) <-> f : R --> NN0 ) )
260259, 247imbi12d 334 . . . . . . . . . . . . 13 |- ( 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 ) ) )
261260spv 2260 . . . . . . . . . . . 12 |- ( 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 ) )
262257, 29, 261sylc 65 . . . . . . . . . . 11 |- ( ( ( 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 )
263262expr 643 . . . . . . . . . 10 |- ( ( ( 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 ) )
264263ralrimdva 2969 . . . . . . . . 9 |- ( ( 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 ) )
26527, 264syl5bi 232 . . . . . . . 8 |- ( ( 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 ) )
266265expcom 451 . . . . . . 7 |- ( 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 ) ) )
267266a2d 29 . . . . . 6 |- ( 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 ) ) )
2688, 12, 16, 20, 24, 267nn0ind 11472 . . . . 5 |- ( M e. NN0 -> ( R e. Fin -> A. f e. ( NN0 ^m R ) ( M Ramsey f ) e. NN0 ) )
269268imp 445 . . . 4 |- ( ( M e. NN0 /\ R e. Fin ) -> A. f e. ( NN0 ^m R ) ( M Ramsey f ) e. NN0 )
270 oveq2 6658 . . . . . 6 |- ( f = F -> ( M Ramsey f ) = ( M Ramsey F ) )
271270eleq1d 2686 . . . . 5 |- ( f = F -> ( ( M Ramsey f ) e. NN0 <-> ( M Ramsey F ) e. NN0 ) )
272271rspccv 3306 . . . 4 |- ( A. f e. ( NN0 ^m R ) ( M Ramsey f ) e. NN0 -> ( F e. ( NN0 ^m R ) -> ( M Ramsey F ) e. NN0 ) )
273269, 272syl 17 . . 3 |- ( ( M e. NN0 /\ R e. Fin ) -> ( F e. ( NN0 ^m R ) -> ( M Ramsey F ) e. NN0 ) )
2744, 273sylbird 250 . 2 |- ( ( M e. NN0 /\ R e. Fin ) -> ( F : R --> NN0 -> ( M Ramsey F ) e. NN0 ) )
2752743impia 1261 1 |- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   <_ cle 10075   - cmin 10266   NNcn 11020   NN0cn0 11292   #chash 13117   sum_csu 14416   Ramsey cram 15703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-ram 15705
This theorem is referenced by:  ramsey  15734
  Copyright terms: Public domain W3C validator