ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seqvalcd Unicode version

Theorem seqvalcd 10125
Description: Value of the sequence builder function. Similar to seq3val 10124 but the classes  D (type of each term) and  C (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.)
Hypotheses
Ref Expression
seqvalcd.m  |-  ( ph  ->  M  e.  ZZ )
seqvalcd.r  |-  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. )
seqvalcd.f0  |-  ( ph  ->  ( F `  M
)  e.  C )
seqvalcd.pl  |-  ( (
ph  /\  ( x  e.  C  /\  y  e.  D ) )  -> 
( x  .+  y
)  e.  C )
seqvalcd.fp1  |-  ( (
ph  /\  x  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( F `  x )  e.  D
)
Assertion
Ref Expression
seqvalcd  |-  ( ph  ->  seq M (  .+  ,  F )  =  ran  R )
Distinct variable groups:    x,  .+ , y, w, z    x, C, y, w, z    x, D, y    x, F, y, w, z    x, M, y, w, z    x, R, y, w, z    ph, x, y, w, z
Allowed substitution hints:    D( z, w)

Proof of Theorem seqvalcd
Dummy variables  a  b  c  k  n  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seqvalcd.m . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
2 seqvalcd.f0 . . . . . 6  |-  ( ph  ->  ( F `  M
)  e.  C )
3 ssv 3085 . . . . . . 7  |-  C  C_  _V
43a1i 9 . . . . . 6  |-  ( ph  ->  C  C_  _V )
5 eqidd 2116 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  (
z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) )  =  ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) )
6 simprr 504 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  ( ZZ>= `  M )  /\  y  e.  C ) )  /\  ( z  =  x  /\  w  =  y ) )  ->  w  =  y )
7 simprl 503 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  ( ZZ>= `  M )  /\  y  e.  C ) )  /\  ( z  =  x  /\  w  =  y ) )  ->  z  =  x )
87fvoveq1d 5750 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  ( ZZ>= `  M )  /\  y  e.  C ) )  /\  ( z  =  x  /\  w  =  y ) )  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( x  +  1
) ) )
96, 8oveq12d 5746 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  ( ZZ>= `  M )  /\  y  e.  C ) )  /\  ( z  =  x  /\  w  =  y ) )  ->  (
w  .+  ( F `  ( z  +  1 ) ) )  =  ( y  .+  ( F `  ( x  +  1 ) ) ) )
10 simprl 503 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  x  e.  ( ZZ>= `  M )
)
11 simprr 504 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  y  e.  C )
12 seqvalcd.pl . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  C  /\  y  e.  D ) )  -> 
( x  .+  y
)  e.  C )
1312ralrimivva 2488 . . . . . . . . . . 11  |-  ( ph  ->  A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C )
14 oveq1 5735 . . . . . . . . . . . . 13  |-  ( x  =  a  ->  (
x  .+  y )  =  ( a  .+  y ) )
1514eleq1d 2183 . . . . . . . . . . . 12  |-  ( x  =  a  ->  (
( x  .+  y
)  e.  C  <->  ( a  .+  y )  e.  C
) )
16 oveq2 5736 . . . . . . . . . . . . 13  |-  ( y  =  b  ->  (
a  .+  y )  =  ( a  .+  b ) )
1716eleq1d 2183 . . . . . . . . . . . 12  |-  ( y  =  b  ->  (
( a  .+  y
)  e.  C  <->  ( a  .+  b )  e.  C
) )
1815, 17cbvral2v 2636 . . . . . . . . . . 11  |-  ( A. x  e.  C  A. y  e.  D  (
x  .+  y )  e.  C  <->  A. a  e.  C  A. b  e.  D  ( a  .+  b
)  e.  C )
1913, 18sylib 121 . . . . . . . . . 10  |-  ( ph  ->  A. a  e.  C  A. b  e.  D  ( a  .+  b
)  e.  C )
2019adantr 272 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  A. a  e.  C  A. b  e.  D  ( a  .+  b )  e.  C
)
21 fveq2 5375 . . . . . . . . . . . 12  |-  ( a  =  ( x  + 
1 )  ->  ( F `  a )  =  ( F `  ( x  +  1
) ) )
2221eleq1d 2183 . . . . . . . . . . 11  |-  ( a  =  ( x  + 
1 )  ->  (
( F `  a
)  e.  D  <->  ( F `  ( x  +  1 ) )  e.  D
) )
23 seqvalcd.fp1 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( F `  x )  e.  D
)
2423ralrimiva 2479 . . . . . . . . . . . . 13  |-  ( ph  ->  A. x  e.  (
ZZ>= `  ( M  + 
1 ) ) ( F `  x )  e.  D )
25 fveq2 5375 . . . . . . . . . . . . . . 15  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
2625eleq1d 2183 . . . . . . . . . . . . . 14  |-  ( x  =  a  ->  (
( F `  x
)  e.  D  <->  ( F `  a )  e.  D
) )
2726cbvralv 2628 . . . . . . . . . . . . 13  |-  ( A. x  e.  ( ZZ>= `  ( M  +  1
) ) ( F `
 x )  e.  D  <->  A. a  e.  (
ZZ>= `  ( M  + 
1 ) ) ( F `  a )  e.  D )
2824, 27sylib 121 . . . . . . . . . . . 12  |-  ( ph  ->  A. a  e.  (
ZZ>= `  ( M  + 
1 ) ) ( F `  a )  e.  D )
2928adantr 272 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  A. a  e.  ( ZZ>= `  ( M  +  1 ) ) ( F `  a
)  e.  D )
30 eluzp1p1 9253 . . . . . . . . . . . 12  |-  ( x  e.  ( ZZ>= `  M
)  ->  ( x  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
3110, 30syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  (
x  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
3222, 29, 31rspcdva 2765 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  ( F `  ( x  +  1 ) )  e.  D )
33 oveq12 5737 . . . . . . . . . . . 12  |-  ( ( a  =  y  /\  b  =  ( F `  ( x  +  1 ) ) )  -> 
( a  .+  b
)  =  ( y 
.+  ( F `  ( x  +  1
) ) ) )
3433eleq1d 2183 . . . . . . . . . . 11  |-  ( ( a  =  y  /\  b  =  ( F `  ( x  +  1 ) ) )  -> 
( ( a  .+  b )  e.  C  <->  ( y  .+  ( F `
 ( x  + 
1 ) ) )  e.  C ) )
3534rspc2gv 2771 . . . . . . . . . 10  |-  ( ( y  e.  C  /\  ( F `  ( x  +  1 ) )  e.  D )  -> 
( A. a  e.  C  A. b  e.  D  ( a  .+  b )  e.  C  ->  ( y  .+  ( F `  ( x  +  1 ) ) )  e.  C ) )
3611, 32, 35syl2anc 406 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  ( A. a  e.  C  A. b  e.  D  ( a  .+  b
)  e.  C  -> 
( y  .+  ( F `  ( x  +  1 ) ) )  e.  C ) )
3720, 36mpd 13 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  (
y  .+  ( F `  ( x  +  1 ) ) )  e.  C )
385, 9, 10, 11, 37ovmpod 5852 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  (
x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )  =  ( y  .+  ( F `  ( x  +  1 ) ) ) )
3938, 37eqeltrd 2191 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  C
) )  ->  (
x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )  e.  C )
40 seqvalcd.r . . . . . 6  |-  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. )
411, 2, 4, 39, 40frecuzrdgrclt 10081 . . . . 5  |-  ( ph  ->  R : om --> ( (
ZZ>= `  M )  X.  C ) )
4241ffnd 5231 . . . 4  |-  ( ph  ->  R  Fn  om )
43 1st2nd2 6027 . . . . . . . . . . . 12  |-  ( u  e.  ( ( ZZ>= `  M )  X.  C
)  ->  u  =  <. ( 1st `  u
) ,  ( 2nd `  u ) >. )
4443adantl 273 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  u  =  <. ( 1st `  u
) ,  ( 2nd `  u ) >. )
4544fveq2d 5379 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  =  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  <. ( 1st `  u ) ,  ( 2nd `  u
) >. ) )
46 df-ov 5731 . . . . . . . . . 10  |-  ( ( 1st `  u ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  u
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  <. ( 1st `  u ) ,  ( 2nd `  u )
>. )
4745, 46syl6eqr 2165 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  =  ( ( 1st `  u ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  u
) ) )
48 xp1st 6017 . . . . . . . . . . 11  |-  ( u  e.  ( ( ZZ>= `  M )  X.  C
)  ->  ( 1st `  u )  e.  (
ZZ>= `  M ) )
4948adantl 273 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( 1st `  u )  e.  (
ZZ>= `  M ) )
50 xp2nd 6018 . . . . . . . . . . . 12  |-  ( u  e.  ( ( ZZ>= `  M )  X.  C
)  ->  ( 2nd `  u )  e.  C
)
5150adantl 273 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( 2nd `  u )  e.  C
)
5251elexd 2670 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( 2nd `  u )  e.  _V )
53 peano2uz 9280 . . . . . . . . . . . 12  |-  ( ( 1st `  u )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  M ) )
5449, 53syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  M ) )
5513adantr 272 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C
)
56 fveq2 5375 . . . . . . . . . . . . . . 15  |-  ( x  =  ( ( 1st `  u )  +  1 )  ->  ( F `  x )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
5756eleq1d 2183 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( 1st `  u )  +  1 )  ->  ( ( F `  x )  e.  D  <->  ( F `  ( ( 1st `  u
)  +  1 ) )  e.  D ) )
5824adantr 272 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  A. x  e.  ( ZZ>= `  ( M  +  1 ) ) ( F `  x
)  e.  D )
59 eluzp1p1 9253 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  u )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  ( M  + 
1 ) ) )
6049, 59syl 14 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  ( M  + 
1 ) ) )
6157, 58, 60rspcdva 2765 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( F `  ( ( 1st `  u
)  +  1 ) )  e.  D )
62 oveq12 5737 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( 2nd `  u )  /\  y  =  ( F `  ( ( 1st `  u
)  +  1 ) ) )  ->  (
x  .+  y )  =  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) ) )
6362eleq1d 2183 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( 2nd `  u )  /\  y  =  ( F `  ( ( 1st `  u
)  +  1 ) ) )  ->  (
( x  .+  y
)  e.  C  <->  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )  e.  C ) )
6463rspc2gv 2771 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  u
)  e.  C  /\  ( F `  ( ( 1st `  u )  +  1 ) )  e.  D )  -> 
( A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C  ->  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) )  e.  C
) )
6551, 61, 64syl2anc 406 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( A. x  e.  C  A. y  e.  D  (
x  .+  y )  e.  C  ->  ( ( 2nd `  u ) 
.+  ( F `  ( ( 1st `  u
)  +  1 ) ) )  e.  C
) )
6655, 65mpd 13 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )  e.  C )
6754, 66opelxpd 4532 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  C ) )
68 oveq1 5735 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  u
)  ->  ( x  +  1 )  =  ( ( 1st `  u
)  +  1 ) )
69 fvoveq1 5751 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  u
)  ->  ( F `  ( x  +  1 ) )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
7069oveq2d 5744 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  u
)  ->  ( y  .+  ( F `  (
x  +  1 ) ) )  =  ( y  .+  ( F `
 ( ( 1st `  u )  +  1 ) ) ) )
7168, 70opeq12d 3679 . . . . . . . . . . 11  |-  ( x  =  ( 1st `  u
)  ->  <. ( x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >.  =  <. ( ( 1st `  u
)  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  u )  +  1 ) ) ) >. )
72 oveq1 5735 . . . . . . . . . . . 12  |-  ( y  =  ( 2nd `  u
)  ->  ( y  .+  ( F `  (
( 1st `  u
)  +  1 ) ) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
7372opeq2d 3678 . . . . . . . . . . 11  |-  ( y  =  ( 2nd `  u
)  ->  <. ( ( 1st `  u )  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >. )
74 eqid 2115 . . . . . . . . . . 11  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. )  =  (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. )
7571, 73, 74ovmpog 5859 . . . . . . . . . 10  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e. 
_V  /\  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  C ) )  -> 
( ( 1st `  u
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  u
) )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>. )
7649, 52, 67, 75syl3anc 1199 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ( 2nd `  u ) )  = 
<. ( ( 1st `  u
)  +  1 ) ,  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>. )
7747, 76eqtrd 2147 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  =  <. (
( 1st `  u
)  +  1 ) ,  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>. )
7877, 67eqeltrd 2191 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  C ) )
7978ralrimiva 2479 . . . . . 6  |-  ( ph  ->  A. u  e.  ( ( ZZ>= `  M )  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  C ) )
80 uzid 9242 . . . . . . . 8  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
811, 80syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
8281, 2opelxpd 4532 . . . . . 6  |-  ( ph  -> 
<. M ,  ( F `
 M ) >.  e.  ( ( ZZ>= `  M
)  X.  C ) )
8379, 82jca 302 . . . . 5  |-  ( ph  ->  ( A. u  e.  ( ( ZZ>= `  M
)  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  C )  /\  <. M ,  ( F `  M )
>.  e.  ( ( ZZ>= `  M )  X.  C
) ) )
84 frecfcl 6256 . . . . 5  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  C )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  C ) )  -> frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) : om --> ( ( ZZ>= `  M
)  X.  C ) )
85 ffn 5230 . . . . 5  |-  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) : om --> ( ( ZZ>= `  M
)  X.  C )  -> frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. )  Fn  om )
8683, 84, 853syl 17 . . . 4  |-  ( ph  -> frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )  Fn  om )
87 fveq2 5375 . . . . . . . 8  |-  ( c  =  (/)  ->  ( R `
 c )  =  ( R `  (/) ) )
88 fveq2 5375 . . . . . . . 8  |-  ( c  =  (/)  ->  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) ) )
8987, 88eqeq12d 2129 . . . . . . 7  |-  ( c  =  (/)  ->  ( ( R `  c )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) `  c )  <->  ( R `  (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) ) ) )
9089imbi2d 229 . . . . . 6  |-  ( c  =  (/)  ->  ( (
ph  ->  ( R `  c )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
) )  <->  ( ph  ->  ( R `  (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) ) ) ) )
91 fveq2 5375 . . . . . . . 8  |-  ( c  =  k  ->  ( R `  c )  =  ( R `  k ) )
92 fveq2 5375 . . . . . . . 8  |-  ( c  =  k  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) )
9391, 92eqeq12d 2129 . . . . . . 7  |-  ( c  =  k  ->  (
( R `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  <->  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
9493imbi2d 229 . . . . . 6  |-  ( c  =  k  ->  (
( ph  ->  ( R `
 c )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  c
) )  <->  ( ph  ->  ( R `  k
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) ) )
95 fveq2 5375 . . . . . . . 8  |-  ( c  =  suc  k  -> 
( R `  c
)  =  ( R `
 suc  k )
)
96 fveq2 5375 . . . . . . . 8  |-  ( c  =  suc  k  -> 
(frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k ) )
9795, 96eqeq12d 2129 . . . . . . 7  |-  ( c  =  suc  k  -> 
( ( R `  c )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  <->  ( R `  suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k ) ) )
9897imbi2d 229 . . . . . 6  |-  ( c  =  suc  k  -> 
( ( ph  ->  ( R `  c )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) `  c ) )  <->  ( ph  ->  ( R `  suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k ) ) ) )
99 fveq2 5375 . . . . . . . 8  |-  ( c  =  n  ->  ( R `  c )  =  ( R `  n ) )
100 fveq2 5375 . . . . . . . 8  |-  ( c  =  n  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  n
) )
10199, 100eqeq12d 2129 . . . . . . 7  |-  ( c  =  n  ->  (
( R `  c
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  c
)  <->  ( R `  n )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  n
) ) )
102101imbi2d 229 . . . . . 6  |-  ( c  =  n  ->  (
( ph  ->  ( R `
 c )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  c
) )  <->  ( ph  ->  ( R `  n
)  =  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  n
) ) ) )
10340fveq1i 5376 . . . . . . . 8  |-  ( R `
 (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )
104 frec0g 6248 . . . . . . . . 9  |-  ( <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  C )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
10582, 104syl 14 . . . . . . . 8  |-  ( ph  ->  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
106103, 105syl5eq 2159 . . . . . . 7  |-  ( ph  ->  ( R `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
107 frec0g 6248 . . . . . . . 8  |-  ( <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  C )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
10882, 107syl 14 . . . . . . 7  |-  ( ph  ->  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
109106, 108eqtr4d 2150 . . . . . 6  |-  ( ph  ->  ( R `  (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) ) )
11041ad2antlr 478 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  R : om --> ( ( ZZ>= `  M )  X.  C
) )
111 simpll 501 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  k  e.  om )
112110, 111ffvelrnd 5510 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  k )  e.  ( ( ZZ>= `  M
)  X.  C ) )
113 xp1st 6017 . . . . . . . . . . 11  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  C
)  ->  ( 1st `  ( R `  k
) )  e.  (
ZZ>= `  M ) )
114112, 113syl 14 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( 1st `  ( R `  k ) )  e.  ( ZZ>= `  M )
)
115 xp2nd 6018 . . . . . . . . . . . 12  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  C
)  ->  ( 2nd `  ( R `  k
) )  e.  C
)
116112, 115syl 14 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( 2nd `  ( R `  k ) )  e.  C )
117116elexd 2670 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( 2nd `  ( R `  k ) )  e. 
_V )
118 peano2uz 9280 . . . . . . . . . . . 12  |-  ( ( 1st `  ( R `
 k ) )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  ( R `  k ) )  +  1 )  e.  (
ZZ>= `  M ) )
119114, 118syl 14 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
)  +  1 )  e.  ( ZZ>= `  M
) )
12013ad2antlr 478 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C
)
121 fveq2 5375 . . . . . . . . . . . . . . 15  |-  ( a  =  ( ( 1st `  ( R `  k
) )  +  1 )  ->  ( F `  a )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
122121eleq1d 2183 . . . . . . . . . . . . . 14  |-  ( a  =  ( ( 1st `  ( R `  k
) )  +  1 )  ->  ( ( F `  a )  e.  D  <->  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) )  e.  D ) )
12328ad2antlr 478 . . . . . . . . . . . . . 14  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  A. a  e.  ( ZZ>= `  ( M  +  1 ) ) ( F `  a
)  e.  D )
124 eluzp1p1 9253 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  ( R `
 k ) )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  ( R `  k ) )  +  1 )  e.  (
ZZ>= `  ( M  + 
1 ) ) )
125114, 124syl 14 . . . . . . . . . . . . . 14  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
)  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
126122, 123, 125rspcdva 2765 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) )  e.  D )
127 oveq12 5737 . . . . . . . . . . . . . . 15  |-  ( ( x  =  ( 2nd `  ( R `  k
) )  /\  y  =  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  ->  (
x  .+  y )  =  ( ( 2nd `  ( R `  k
) )  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) ) )
128127eleq1d 2183 . . . . . . . . . . . . . 14  |-  ( ( x  =  ( 2nd `  ( R `  k
) )  /\  y  =  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  ->  (
( x  .+  y
)  e.  C  <->  ( ( 2nd `  ( R `  k ) )  .+  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )  e.  C ) )
129128rspc2gv 2771 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( R `  k )
)  e.  C  /\  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) )  e.  D )  -> 
( A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C  ->  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  C
) )
130116, 126, 129syl2anc 406 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( A. x  e.  C  A. y  e.  D  ( x  .+  y )  e.  C  ->  (
( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  C
) )
131120, 130mpd 13 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  C
)
132119, 131opelxpd 4532 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  <. (
( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 2nd `  ( R `  k
) )  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) )
>.  e.  ( ( ZZ>= `  M )  X.  C
) )
133 oveq1 5735 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( x  +  1 )  =  ( ( 1st `  ( R `  k )
)  +  1 ) )
134 fvoveq1 5751 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( F `  ( x  +  1 ) )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
135134oveq2d 5744 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( y  .+  ( F `  (
x  +  1 ) ) )  =  ( y  .+  ( F `
 ( ( 1st `  ( R `  k
) )  +  1 ) ) ) )
136133, 135opeq12d 3679 . . . . . . . . . . 11  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  <. ( x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >.  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) ) >. )
137 oveq1 5735 . . . . . . . . . . . 12  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  ( y  .+  ( F `  (
( 1st `  ( R `  k )
)  +  1 ) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
138137opeq2d 3678 . . . . . . . . . . 11  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) )
>.  =  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) >. )
139136, 138, 74ovmpog 5859 . . . . . . . . . 10  |-  ( ( ( 1st `  ( R `  k )
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  ( R `  k ) )  e. 
_V  /\  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  C ) )  -> 
( ( 1st `  ( R `  k )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 2nd `  ( R `  k
) )  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) )
>. )
140114, 117, 132, 139syl3anc 1199 . . . . . . . . 9  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 2nd `  ( R `  k
) )  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) )
>. )
14179ad2antlr 478 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  A. u  e.  ( ( ZZ>= `  M
)  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  C ) )
14282ad2antlr 478 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  <. M , 
( F `  M
) >.  e.  ( (
ZZ>= `  M )  X.  C ) )
143 frecsuc 6258 . . . . . . . . . . 11  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  C )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  C )  /\  k  e.  om )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
144141, 142, 111, 143syl3anc 1199 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
145 simpr 109 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )
146145fveq2d 5379 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  ( R `  k ) )  =  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
147 1st2nd2 6027 . . . . . . . . . . . . 13  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  C
)  ->  ( R `  k )  =  <. ( 1st `  ( R `
 k ) ) ,  ( 2nd `  ( R `  k )
) >. )
148112, 147syl 14 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  k )  =  <. ( 1st `  ( R `  k )
) ,  ( 2nd `  ( R `  k
) ) >. )
149148fveq2d 5379 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  ( R `  k ) )  =  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. ) )
150 df-ov 5731 . . . . . . . . . . 11  |-  ( ( 1st `  ( R `
 k ) ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  ( R `  k )
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. )
151149, 150syl6eqr 2165 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  ( R `  k ) )  =  ( ( 1st `  ( R `  k )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  ( R `  k )
) ) )
152144, 146, 1513eqtr2d 2153 . . . . . . . . 9  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k )  =  ( ( 1st `  ( R `  k )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ( 2nd `  ( R `  k )
) ) )
15344fveq2d 5379 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  u ) ,  ( 2nd `  u )
>. ) )
154 df-ov 5731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  u ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  u
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  u ) ,  ( 2nd `  u )
>. )
155153, 154syl6eqr 2165 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  ( ( 1st `  u
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  u
) ) )
156 fvoveq1 5751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  ( 1st `  u
)  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
157156oveq2d 5744 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  ( 1st `  u
)  ->  ( w  .+  ( F `  (
z  +  1 ) ) )  =  ( w  .+  ( F `
 ( ( 1st `  u )  +  1 ) ) ) )
158 oveq1 5735 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  ( 2nd `  u
)  ->  ( w  .+  ( F `  (
( 1st `  u
)  +  1 ) ) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
159 eqid 2115 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) )  =  ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) )
160157, 158, 159ovmpog 5859 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e.  C  /\  ( ( 2nd `  u ) 
.+  ( F `  ( ( 1st `  u
)  +  1 ) ) )  e.  C
)  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
16149, 51, 66, 160syl3anc 1199 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
162161, 66eqeltrd 2191 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  e.  C
)
16354, 162opelxpd 4532 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.  e.  ( ( ZZ>= `  M
)  X.  C ) )
164 oveq1 5735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( 1st `  u
)  ->  ( x
( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y ) )
16568, 164opeq12d 3679 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( 1st `  u
)  ->  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )
166 oveq2 5736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( 2nd `  u
)  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) )
167166opeq2d 3678 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( 2nd `  u
)  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
168 eqid 2115 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )  =  (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
169165, 167, 168ovmpog 5859 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e. 
_V  /\  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  u
) )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
17049, 52, 163, 169syl3anc 1199 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  u ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  u
) )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
171155, 170eqtrd 2147 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
172171, 163eqeltrd 2191 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  C ) )
173172ralrimiva 2479 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. u  e.  ( ( ZZ>= `  M )  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  C ) )
174173ad2antlr 478 . . . . . . . . . . . . . 14  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  A. u  e.  ( ( ZZ>= `  M
)  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  C ) )
175 frecsuc 6258 . . . . . . . . . . . . . 14  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  C ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  C )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  C )  /\  k  e.  om )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
176174, 142, 111, 175syl3anc 1199 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
17740fveq1i 5376 . . . . . . . . . . . . 13  |-  ( R `
 suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  suc  k )
17840fveq1i 5376 . . . . . . . . . . . . . 14  |-  ( R `
 k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
)
179178fveq2i 5378 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  ( R `  k
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) )
180176, 177, 1793eqtr4g 2172 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  suc  k )  =  ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) `  ( R `
 k ) ) )
181148fveq2d 5379 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  ( R `  k ) )  =  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. ) )
182180, 181eqtrd 2147 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  suc  k )  =  ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) `  <. ( 1st `  ( R `  k ) ) ,  ( 2nd `  ( R `  k )
) >. ) )
183 df-ov 5731 . . . . . . . . . . 11  |-  ( ( 1st `  ( R `
 k ) ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  ( R `  k )
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. )
184182, 183syl6eqr 2165 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  suc  k )  =  ( ( 1st `  ( R `  k
) ) ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ( 2nd `  ( R `  k )
) ) )
185 fvoveq1 5751 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( 1st `  ( R `  k )
)  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
186185oveq2d 5744 . . . . . . . . . . . . . . 15  |-  ( z  =  ( 1st `  ( R `  k )
)  ->  ( w  .+  ( F `  (
z  +  1 ) ) )  =  ( w  .+  ( F `
 ( ( 1st `  ( R `  k
) )  +  1 ) ) ) )
187 oveq1 5735 . . . . . . . . . . . . . . 15  |-  ( w  =  ( 2nd `  ( R `  k )
)  ->  ( w  .+  ( F `  (
( 1st `  ( R `  k )
)  +  1 ) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
188186, 187, 159ovmpog 5859 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  ( R `  k )
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  ( R `  k ) )  e.  C  /\  ( ( 2nd `  ( R `
 k ) ) 
.+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  C
)  ->  ( ( 1st `  ( R `  k ) ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k )
) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
189114, 116, 131, 188syl3anc 1199 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
190189, 131eqeltrd 2191 . . . . . . . . . . . 12  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) )  e.  C )
191119, 190opelxpd 4532 . . . . . . . . . . 11  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  <. (
( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  e.  ( ( ZZ>= `  M
)  X.  C ) )
192 oveq1 5735 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( x
( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y ) )
193133, 192opeq12d 3679 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )
194 oveq2 5736 . . . . . . . . . . . . 13  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  ( ( 1st `  ( R `  k ) ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) )
195194opeq2d 3678 . . . . . . . . . . . 12  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
196193, 195, 168ovmpog 5859 . . . . . . . . . . 11  |-  ( ( ( 1st `  ( R `  k )
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  ( R `  k ) )  e. 
_V  /\  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  e.  ( ( ZZ>= `  M
)  X.  C ) )  ->  ( ( 1st `  ( R `  k ) ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  C  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
197114, 117, 191, 196syl3anc 1199 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  (
( 1st `  ( R `  k )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  C  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
198189opeq2d 3678 . . . . . . . . . 10  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  <. (
( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  C  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  =  <. ( ( 1st `  ( R `  k
) )  +  1 ) ,  ( ( 2nd `  ( R `
 k ) ) 
.+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) >. )
199184, 197, 1983eqtrd 2151 . . . . . . . . 9  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  suc  k )  =  <. ( ( 1st `  ( R `  k
) )  +  1 ) ,  ( ( 2nd `  ( R `
 k ) ) 
.+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) >. )
200140, 152, 1993eqtr4rd 2158 . . . . . . . 8  |-  ( ( ( k  e.  om  /\ 
ph )  /\  ( R `  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( R `  suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. ) `  suc  k ) )
201200exp31 359 . . . . . . 7  |-  ( k  e.  om  ->  ( ph  ->  ( ( R `
 k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
)  ->  ( R `  suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  suc  k ) ) ) )
202201a2d 26 . . . . . 6  |-  ( k  e.  om  ->  (
( ph  ->  ( R `
 k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )  ->  ( ph  ->  ( R `  suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  suc  k ) ) ) )
20390, 94, 98, 102, 109, 202finds 4474 . . . . 5  |-  ( n  e.  om  ->  ( ph  ->  ( R `  n )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  n
) ) )
204203impcom 124 . . . 4  |-  ( (
ph  /\  n  e.  om )  ->  ( R `  n )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  n
) )
20542, 86, 204eqfnfvd 5475 . . 3  |-  ( ph  ->  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. )
)
206205rneqd 4728 . 2  |-  ( ph  ->  ran  R  =  ran frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
(