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

Theorem seq3val 9862
Description: Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 9868, seq3-1 9865 and seq3p1 9872, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.)
Hypotheses
Ref Expression
seq3val.m  |-  ( ph  ->  M  e.  ZZ )
seq3val.r  |-  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. )
seq3val.f  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  S
)
seq3val.pl  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
Assertion
Ref Expression
seq3val  |-  ( ph  ->  seq M (  .+  ,  F )  =  ran  R )
Distinct variable groups:    x,  .+ , y, w, z    x, F, y, w, z    x, M, y, w, z    x, R, y, w, z    x, S, y, w, z    ph, x, y, w, z

Proof of Theorem seq3val
Dummy variables  a  b  k  c  n  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 seq3val.m . . . . . 6  |-  ( ph  ->  M  e.  ZZ )
2 fveq2 5299 . . . . . . . 8  |-  ( x  =  M  ->  ( F `  x )  =  ( F `  M ) )
32eleq1d 2156 . . . . . . 7  |-  ( x  =  M  ->  (
( F `  x
)  e.  S  <->  ( F `  M )  e.  S
) )
4 seq3val.f . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( ZZ>= `  M )
)  ->  ( F `  x )  e.  S
)
54ralrimiva 2446 . . . . . . 7  |-  ( ph  ->  A. x  e.  (
ZZ>= `  M ) ( F `  x )  e.  S )
6 uzid 9023 . . . . . . . 8  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
71, 6syl 14 . . . . . . 7  |-  ( ph  ->  M  e.  ( ZZ>= `  M ) )
83, 5, 7rspcdva 2727 . . . . . 6  |-  ( ph  ->  ( F `  M
)  e.  S )
9 ssv 3046 . . . . . . 7  |-  S  C_  _V
109a1i 9 . . . . . 6  |-  ( ph  ->  S  C_  _V )
11 seq3val.pl . . . . . . 7  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  .+  y
)  e.  S )
124, 11iseqovex 9858 . . . . . 6  |-  ( (
ph  /\  ( x  e.  ( ZZ>= `  M )  /\  y  e.  S
) )  ->  (
x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )  e.  S )
13 seq3val.r . . . . . 6  |-  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. )
141, 8, 10, 12, 13frecuzrdgrclt 9810 . . . . 5  |-  ( ph  ->  R : om --> ( (
ZZ>= `  M )  X.  S ) )
15 ffn 5155 . . . . 5  |-  ( R : om --> ( (
ZZ>= `  M )  X.  S )  ->  R  Fn  om )
1614, 15syl 14 . . . 4  |-  ( ph  ->  R  Fn  om )
17 1st2nd2 5937 . . . . . . . . . . . 12  |-  ( u  e.  ( ( ZZ>= `  M )  X.  S
)  ->  u  =  <. ( 1st `  u
) ,  ( 2nd `  u ) >. )
1817adantl 271 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  u  =  <. ( 1st `  u
) ,  ( 2nd `  u ) >. )
1918fveq2d 5303 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
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
) >. ) )
20 df-ov 5647 . . . . . . . . . 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 )
>. )
2119, 20syl6eqr 2138 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
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
) ) )
22 xp1st 5928 . . . . . . . . . . 11  |-  ( u  e.  ( ( ZZ>= `  M )  X.  S
)  ->  ( 1st `  u )  e.  (
ZZ>= `  M ) )
2322adantl 271 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( 1st `  u )  e.  (
ZZ>= `  M ) )
24 xp2nd 5929 . . . . . . . . . . . 12  |-  ( u  e.  ( ( ZZ>= `  M )  X.  S
)  ->  ( 2nd `  u )  e.  S
)
2524adantl 271 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( 2nd `  u )  e.  S
)
2625elexd 2632 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( 2nd `  u )  e.  _V )
27 peano2uz 9061 . . . . . . . . . . . 12  |-  ( ( 1st `  u )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  M ) )
2823, 27syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  u )  +  1 )  e.  (
ZZ>= `  M ) )
2911caovclg 5789 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  S  /\  b  e.  S ) )  -> 
( a  .+  b
)  e.  S )
3029adantlr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  /\  ( a  e.  S  /\  b  e.  S ) )  -> 
( a  .+  b
)  e.  S )
31 fveq2 5299 . . . . . . . . . . . . . 14  |-  ( x  =  ( ( 1st `  u )  +  1 )  ->  ( F `  x )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
3231eleq1d 2156 . . . . . . . . . . . . 13  |-  ( x  =  ( ( 1st `  u )  +  1 )  ->  ( ( F `  x )  e.  S  <->  ( F `  ( ( 1st `  u
)  +  1 ) )  e.  S ) )
335adantr 270 . . . . . . . . . . . . 13  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  A. x  e.  ( ZZ>= `  M )
( F `  x
)  e.  S )
3432, 33, 28rspcdva 2727 . . . . . . . . . . . 12  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( F `  ( ( 1st `  u
)  +  1 ) )  e.  S )
3530, 25, 34caovcld 5790 . . . . . . . . . . 11  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )  e.  S )
36 opelxpi 4467 . . . . . . . . . . 11  |-  ( ( ( ( 1st `  u
)  +  1 )  e.  ( ZZ>= `  M
)  /\  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )  e.  S )  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u ) 
.+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  S ) )
3728, 35, 36syl2anc 403 . . . . . . . . . 10  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  S ) )
38 oveq1 5651 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  u
)  ->  ( x  +  1 )  =  ( ( 1st `  u
)  +  1 ) )
39 fvoveq1 5667 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  u
)  ->  ( F `  ( x  +  1 ) )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
4039oveq2d 5660 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  u
)  ->  ( y  .+  ( F `  (
x  +  1 ) ) )  =  ( y  .+  ( F `
 ( ( 1st `  u )  +  1 ) ) ) )
4138, 40opeq12d 3628 . . . . . . . . . . 11  |-  ( x  =  ( 1st `  u
)  ->  <. ( x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >.  =  <. ( ( 1st `  u
)  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  u )  +  1 ) ) ) >. )
42 oveq1 5651 . . . . . . . . . . . 12  |-  ( y  =  ( 2nd `  u
)  ->  ( y  .+  ( F `  (
( 1st `  u
)  +  1 ) ) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
4342opeq2d 3627 . . . . . . . . . . 11  |-  ( y  =  ( 2nd `  u
)  ->  <. ( ( 1st `  u )  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >. )
44 eqid 2088 . . . . . . . . . . 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 ) ) ) >. )
4541, 43, 44ovmpt2g 5771 . . . . . . . . . 10  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e. 
_V  /\  <. ( ( 1st `  u )  +  1 ) ,  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) >.  e.  ( ( ZZ>= `  M )  X.  S ) )  -> 
( ( 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 ) ) )
>. )
4623, 26, 37, 45syl3anc 1174 . . . . . . . . 9  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 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 ) ) )
>. )
4721, 46eqtrd 2120 . . . . . . . 8  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  =  <. (
( 1st `  u
)  +  1 ) ,  ( ( 2nd `  u )  .+  ( F `  ( ( 1st `  u )  +  1 ) ) )
>. )
4847, 37eqeltrd 2164 . . . . . . 7  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  S ) )
4948ralrimiva 2446 . . . . . 6  |-  ( ph  ->  A. u  e.  ( ( ZZ>= `  M )  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  S ) )
50 opelxpi 4467 . . . . . . 7  |-  ( ( M  e.  ( ZZ>= `  M )  /\  ( F `  M )  e.  S )  ->  <. M , 
( F `  M
) >.  e.  ( (
ZZ>= `  M )  X.  S ) )
517, 8, 50syl2anc 403 . . . . . 6  |-  ( ph  -> 
<. M ,  ( F `
 M ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )
5249, 51jca 300 . . . . 5  |-  ( ph  ->  ( A. u  e.  ( ( ZZ>= `  M
)  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  S )  /\  <. M ,  ( F `  M )
>.  e.  ( ( ZZ>= `  M )  X.  S
) ) )
53 frecfcl 6162 . . . . 5  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  S )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  S ) )  -> frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) : om --> ( ( ZZ>= `  M
)  X.  S ) )
54 ffn 5155 . . . . 5  |-  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) : om --> ( ( ZZ>= `  M
)  X.  S )  -> frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. )  Fn  om )
5552, 53, 543syl 17 . . . 4  |-  ( ph  -> frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )  Fn  om )
56 fveq2 5299 . . . . . . . 8  |-  ( c  =  (/)  ->  ( R `
 c )  =  ( R `  (/) ) )
57 fveq2 5299 . . . . . . . 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
) >. ) `  (/) ) )
5856, 57eqeq12d 2102 . . . . . . 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
) >. ) `  (/) ) ) )
5958imbi2d 228 . . . . . 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
) >. ) `  (/) ) ) ) )
60 fveq2 5299 . . . . . . . 8  |-  ( c  =  k  ->  ( R `  c )  =  ( R `  k ) )
61 fveq2 5299 . . . . . . . 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
) )
6260, 61eqeq12d 2102 . . . . . . 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
) ) )
6362imbi2d 228 . . . . . 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
) ) ) )
64 fveq2 5299 . . . . . . . 8  |-  ( c  =  suc  k  -> 
( R `  c
)  =  ( R `
 suc  k )
)
65 fveq2 5299 . . . . . . . 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 ) )
6664, 65eqeq12d 2102 . . . . . . 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 ) ) )
6766imbi2d 228 . . . . . 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 ) ) ) )
68 fveq2 5299 . . . . . . . 8  |-  ( c  =  n  ->  ( R `  c )  =  ( R `  n ) )
69 fveq2 5299 . . . . . . . 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
) )
7068, 69eqeq12d 2102 . . . . . . 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
) ) )
7170imbi2d 228 . . . . . 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
) ) ) )
7213fveq1i 5300 . . . . . . . 8  |-  ( R `
 (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )
73 frec0g 6154 . . . . . . . . 9  |-  ( <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  S )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
7451, 73syl 14 . . . . . . . 8  |-  ( ph  ->  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
7572, 74syl5eq 2132 . . . . . . 7  |-  ( ph  ->  ( R `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
76 frec0g 6154 . . . . . . . 8  |-  ( <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  S )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
7751, 76syl 14 . . . . . . 7  |-  ( ph  ->  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) )  = 
<. M ,  ( F `
 M ) >.
)
7875, 77eqtr4d 2123 . . . . . 6  |-  ( ph  ->  ( R `  (/) )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  (/) ) )
7914ad2antlr 473 . . . . . . . . . . . 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.  S
) )
80 simpll 496 . . . . . . . . . . . 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 )
8179, 80ffvelrnd 5429 . . . . . . . . . . 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.  S ) )
82 xp1st 5928 . . . . . . . . . . 11  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  S
)  ->  ( 1st `  ( R `  k
) )  e.  (
ZZ>= `  M ) )
8381, 82syl 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 )
)
84 xp2nd 5929 . . . . . . . . . . . 12  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  S
)  ->  ( 2nd `  ( R `  k
) )  e.  S
)
8581, 84syl 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.  S )
8685elexd 2632 . . . . . . . . . 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 )
8729adantll 460 . . . . . . . . . . . . . . 15  |-  ( ( ( k  e.  om  /\ 
ph )  /\  (
a  e.  S  /\  b  e.  S )
)  ->  ( a  .+  b )  e.  S
)
8887adantlr 461 . . . . . . . . . . . . . 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  e.  S  /\  b  e.  S
) )  ->  (
a  .+  b )  e.  S )
89 fveq2 5299 . . . . . . . . . . . . . . . 16  |-  ( a  =  ( ( 1st `  ( R `  k
) )  +  1 )  ->  ( F `  a )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
9089eleq1d 2156 . . . . . . . . . . . . . . 15  |-  ( a  =  ( ( 1st `  ( R `  k
) )  +  1 )  ->  ( ( F `  a )  e.  S  <->  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) )  e.  S ) )
91 fveq2 5299 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  a  ->  ( F `  x )  =  ( F `  a ) )
9291eleq1d 2156 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  a  ->  (
( F `  x
)  e.  S  <->  ( F `  a )  e.  S
) )
9392cbvralv 2590 . . . . . . . . . . . . . . . . 17  |-  ( A. x  e.  ( ZZ>= `  M ) ( F `
 x )  e.  S  <->  A. a  e.  (
ZZ>= `  M ) ( F `  a )  e.  S )
945, 93sylib 120 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. a  e.  (
ZZ>= `  M ) ( F `  a )  e.  S )
9594ad2antlr 473 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
( F `  a
)  e.  S )
96 peano2uz 9061 . . . . . . . . . . . . . . . 16  |-  ( ( 1st `  ( R `
 k ) )  e.  ( ZZ>= `  M
)  ->  ( ( 1st `  ( R `  k ) )  +  1 )  e.  (
ZZ>= `  M ) )
9783, 96syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) )
9890, 95, 97rspcdva 2727 . . . . . . . . . . . . . 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
) )  ->  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) )  e.  S )
9988, 85, 98caovcld 5790 . . . . . . . . . . . . 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
) )  ->  (
( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  S
)
100 fvoveq1 5667 . . . . . . . . . . . . . . 15  |-  ( z  =  ( 1st `  ( R `  k )
)  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
101100oveq2d 5660 . . . . . . . . . . . . . 14  |-  ( z  =  ( 1st `  ( R `  k )
)  ->  ( w  .+  ( F `  (
z  +  1 ) ) )  =  ( w  .+  ( F `
 ( ( 1st `  ( R `  k
) )  +  1 ) ) ) )
102 oveq1 5651 . . . . . . . . . . . . . 14  |-  ( w  =  ( 2nd `  ( R `  k )
)  ->  ( w  .+  ( F `  (
( 1st `  ( R `  k )
)  +  1 ) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
103 eqid 2088 . . . . . . . . . . . . . 14  |-  ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) )  =  ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) )
104101, 102, 103ovmpt2g 5771 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  ( R `  k )
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  ( R `  k ) )  e.  S  /\  ( ( 2nd `  ( R `
 k ) ) 
.+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) )  e.  S
)  ->  ( ( 1st `  ( R `  k ) ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k )
) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
10583, 85, 99, 104syl3anc 1174 . . . . . . . . . . . 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.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
106105opeq2d 3627 . . . . . . . . . . 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.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  =  <. ( ( 1st `  ( R `  k
) )  +  1 ) ,  ( ( 2nd `  ( R `
 k ) ) 
.+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) >. )
107105, 99eqeltrd 2164 . . . . . . . . . . . 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.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) )  e.  S )
108 opelxpi 4467 . . . . . . . . . . . 12  |-  ( ( ( ( 1st `  ( R `  k )
)  +  1 )  e.  ( ZZ>= `  M
)  /\  ( ( 1st `  ( R `  k ) ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k )
) )  e.  S
)  ->  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )
10997, 107, 108syl2anc 403 . . . . . . . . . . 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.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )
110106, 109eqeltrrd 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
) )  ->  <. (
( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 2nd `  ( R `  k
) )  .+  ( F `  ( ( 1st `  ( R `  k ) )  +  1 ) ) )
>.  e.  ( ( ZZ>= `  M )  X.  S
) )
111 oveq1 5651 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( x  +  1 )  =  ( ( 1st `  ( R `  k )
)  +  1 ) )
112 fvoveq1 5667 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( F `  ( x  +  1 ) )  =  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) )
113112oveq2d 5660 . . . . . . . . . . . 12  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( y  .+  ( F `  (
x  +  1 ) ) )  =  ( y  .+  ( F `
 ( ( 1st `  ( R `  k
) )  +  1 ) ) ) )
114111, 113opeq12d 3628 . . . . . . . . . . 11  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  <. ( x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >.  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( y  .+  ( F `  ( ( 1st `  ( R `
 k ) )  +  1 ) ) ) >. )
115 oveq1 5651 . . . . . . . . . . . 12  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  ( y  .+  ( F `  (
( 1st `  ( R `  k )
)  +  1 ) ) )  =  ( ( 2nd `  ( R `  k )
)  .+  ( F `  ( ( 1st `  ( R `  k )
)  +  1 ) ) ) )
116115opeq2d 3627 . . . . . . . . . . 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 ) ) ) >. )
117114, 116, 44ovmpt2g 5771 . . . . . . . . . 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.  S ) )  -> 
( ( 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 ) ) )
>. )
11883, 86, 110, 117syl3anc 1174 . . . . . . . . 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 ) ) )
>. )
11949ad2antlr 473 . . . . . . . . . . . 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. u  e.  ( ( ZZ>= `  M
)  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  S ) )
12051ad2antlr 473 . . . . . . . . . . . 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
) )  ->  <. M , 
( F `  M
) >.  e.  ( (
ZZ>= `  M )  X.  S ) )
121 frecsuc 6164 . . . . . . . . . . . 12  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) `  u
)  e.  ( (
ZZ>= `  M )  X.  S )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  S )  /\  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
) ) )
122119, 120, 80, 121syl3anc 1174 . . . . . . . . . . 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
) )  ->  (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
) ) )
123 simpr 108 . . . . . . . . . . . 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 )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( y  .+  ( F `
 ( x  + 
1 ) ) )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
) )
124123fveq2d 5303 . . . . . . . . . . 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
) ) ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
125122, 124eqtr4d 2123 . . . . . . . . . 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
) ) ) >.
) `  ( R `  k ) ) )
126 1st2nd2 5937 . . . . . . . . . . . . 13  |-  ( ( R `  k )  e.  ( ( ZZ>= `  M )  X.  S
)  ->  ( R `  k )  =  <. ( 1st `  ( R `
 k ) ) ,  ( 2nd `  ( R `  k )
) >. )
12781, 126syl 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
) ) >. )
128127fveq2d 5303 . . . . . . . . . . 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 ) )
>. ) )
129 df-ov 5647 . . . . . . . . . . 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 ) )
>. )
130128, 129syl6eqr 2138 . . . . . . . . . 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 )
) ) )
131125, 130eqtrd 2120 . . . . . . . . 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 )
) ) )
13213fveq1i 5300 . . . . . . . . . . . . . . 15  |-  ( R `
 suc  k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  suc  k )
13318fveq2d 5303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  u ) ,  ( 2nd `  u )
>. ) )
134 df-ov 5647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  u ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  u
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  u ) ,  ( 2nd `  u )
>. )
135133, 134syl6eqr 2138 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  ( ( 1st `  u
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  u
) ) )
136 fvoveq1 5667 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  ( 1st `  u
)  ->  ( F `  ( z  +  1 ) )  =  ( F `  ( ( 1st `  u )  +  1 ) ) )
137136oveq2d 5660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  ( 1st `  u
)  ->  ( w  .+  ( F `  (
z  +  1 ) ) )  =  ( w  .+  ( F `
 ( ( 1st `  u )  +  1 ) ) ) )
138 oveq1 5651 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  ( 2nd `  u
)  ->  ( w  .+  ( F `  (
( 1st `  u
)  +  1 ) ) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
139137, 138, 103ovmpt2g 5771 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e.  S  /\  ( ( 2nd `  u ) 
.+  ( F `  ( ( 1st `  u
)  +  1 ) ) )  e.  S
)  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
14023, 25, 35, 139syl3anc 1174 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  =  ( ( 2nd `  u
)  .+  ( F `  ( ( 1st `  u
)  +  1 ) ) ) )
141140, 35eqeltrd 2164 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  e.  S
)
142 opelxpi 4467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 1st `  u
)  +  1 )  e.  ( ZZ>= `  M
)  /\  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u
) )  e.  S
)  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )
14328, 141, 142syl2anc 403 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )
144 oveq1 5651 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( 1st `  u
)  ->  ( x
( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y ) )
14538, 144opeq12d 3628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( 1st `  u
)  ->  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )
146 oveq2 5652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( 2nd `  u
)  ->  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) )
147146opeq2d 3627 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( 2nd `  u
)  ->  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
148 eqid 2088 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )  =  (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
149145, 147, 148ovmpt2g 5771 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 1st `  u
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  u )  e. 
_V  /\  <. ( ( 1st `  u )  +  1 ) ,  ( ( 1st `  u
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  u ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  u
) )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
15023, 26, 143, 149syl3anc 1174 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  u ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  u
) )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
151135, 150eqtrd 2120 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  =  <. ( ( 1st `  u
)  +  1 ) ,  ( ( 1st `  u ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  u ) ) >.
)
152151, 143eqeltrd 2164 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  u  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  S ) )
153152ralrimiva 2446 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. u  e.  ( ( ZZ>= `  M )  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  S ) )
154153ad2antlr 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  u )  e.  ( ( ZZ>= `  M
)  X.  S ) )
155 frecsuc 6164 . . . . . . . . . . . . . . . 16  |-  ( ( A. u  e.  ( ( ZZ>= `  M )  X.  S ) ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  u )  e.  ( ( ZZ>= `  M )  X.  S )  /\  <. M ,  ( F `  M ) >.  e.  ( ( ZZ>= `  M )  X.  S )  /\  k  e.  om )  ->  (frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( 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.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
156154, 120, 80, 155syl3anc 1174 . . . . . . . . . . . . . . 15  |-  ( ( ( 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.  S  |->  ( 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.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
157132, 156syl5eq 2132 . . . . . . . . . . . . . 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
) )  ->  ( R `  suc  k )  =  ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) `  (frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) ) )
15813fveq1i 5300 . . . . . . . . . . . . . . 15  |-  ( R `
 k )  =  (frec ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ,  <. M , 
( F `  M
) >. ) `  k
)
159158fveq2i 5302 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. ) `  ( R `  k
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  (frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ,  <. M , 
( F `  M
) >. ) `  k
) )
160157, 159syl6eqr 2138 . . . . . . . . . . . . 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
) )  ->  ( R `  suc  k )  =  ( ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) `  ( R `
 k ) ) )
161127fveq2d 5303 . . . . . . . . . . . . 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
) )  ->  (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  ( R `  k ) )  =  ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. ) )
162160, 161eqtrd 2120 . . . . . . . . . . . 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.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) `  <. ( 1st `  ( R `  k ) ) ,  ( 2nd `  ( R `  k )
) >. ) )
163 df-ov 5647 . . . . . . . . . . . 12  |-  ( ( 1st `  ( R `
 k ) ) ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  ( R `  k )
) )  =  ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) `  <. ( 1st `  ( R `  k
) ) ,  ( 2nd `  ( R `
 k ) )
>. )
164162, 163syl6eqr 2138 . . . . . . . . . . 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 )  =  ( ( 1st `  ( R `  k
) ) ( x  e.  ( ZZ>= `  M
) ,  y  e. 
_V  |->  <. ( x  + 
1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. ) ( 2nd `  ( R `  k )
) ) )
165 oveq1 5651 . . . . . . . . . . . . . 14  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  ( x
( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y ) )
166111, 165opeq12d 3628 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  ( R `  k )
)  ->  <. ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>. )
167 oveq2 5652 . . . . . . . . . . . . . 14  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  ( ( 1st `  ( R `  k ) ) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y )  =  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) )
168167opeq2d 3627 . . . . . . . . . . . . 13  |-  ( y  =  ( 2nd `  ( R `  k )
)  ->  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) y )
>.  =  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
169166, 168, 148ovmpt2g 5771 . . . . . . . . . . . 12  |-  ( ( ( 1st `  ( R `  k )
)  e.  ( ZZ>= `  M )  /\  ( 2nd `  ( R `  k ) )  e. 
_V  /\  <. ( ( 1st `  ( R `
 k ) )  +  1 ) ,  ( ( 1st `  ( R `  k )
) ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.  e.  ( ( ZZ>= `  M
)  X.  S ) )  ->  ( ( 1st `  ( R `  k ) ) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( x ( z  e.  ( ZZ>= `  M ) ,  w  e.  S  |->  ( w 
.+  ( F `  ( z  +  1 ) ) ) ) y ) >. )
( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
17083, 86, 109, 169syl3anc 1174 . . . . . . . . . . 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 )
) ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. ( x  +  1 ) ,  ( x ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) y ) >.
) ( 2nd `  ( R `  k )
) )  =  <. ( ( 1st `  ( R `  k )
)  +  1 ) ,  ( ( 1st `  ( R `  k
) ) ( z  e.  ( ZZ>= `  M
) ,  w  e.  S  |->  ( w  .+  ( F `  ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k
) ) ) >.
)
171164, 170eqtrd 2120 . . . . . . . . . 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
) )  +  1 ) ,  ( ( 1st `  ( R `
 k ) ) ( z  e.  (
ZZ>= `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
 ( z  +  1 ) ) ) ) ( 2nd `  ( R `  k )
) ) >. )
172171, 106eqtrd 2120 . . . . . . . . 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 ) ) ) >. )
173118, 131, 1723eqtr4rd 2131 . . . . . . . 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 ) )
174173exp31 356 . . . . . . 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 ) ) ) )
175174a2d 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 ) ) ) )
17659, 63, 67, 71, 78, 175finds 4413 . . . . 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
) ) )
177176impcom 123 . . . 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
) )
17816, 55, 177eqfnfvd 5394 . . 3  |-  ( ph  ->  R  = frec ( ( x  e.  ( ZZ>= `  M ) ,  y  e.  _V  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. )
)
179178rneqd 4660 . 2  |-  ( ph  ->  ran  R  =  ran frec ( ( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. ) )
180 dfseq3-2 9843 . 2  |-  seq M
(  .+  ,  F
)  =  ran frec (
( x  e.  (
ZZ>= `  M ) ,  y  e.  _V  |->  <.
( x  +  1 ) ,  ( y 
.+  ( F `  ( x  +  1
) ) ) >.
) ,  <. M , 
( F `  M
) >. )
181179, 180syl6reqr 2139 1  |-  ( ph  ->  seq M (  .+  ,  F )  =  ran  R )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1289    e. wcel 1438   A.wral 2359   _Vcvv 2619    C_ wss 2999   (/)c0 3286   <.cop 3447   suc csuc 4190   omcom 4403    X. cxp 4434   ran crn 4437    Fn wfn 5005   -->wf 5006   ` cfv 5010  (class class class)co 5644    |-> cmpt2 5646   1stc1st 5901   2ndc2nd 5902  freccfrec 6147   1c1 7341    + caddc 7343   ZZcz 8740   ZZ>=cuz 9009    seqcseq 9840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3952  ax-sep 3955  ax-nul 3963  ax-pow 4007  ax-pr 4034  ax-un 4258  ax-setind 4351  ax-iinf 4401  ax-cnex 7426  ax-resscn 7427  ax-1cn 7428  ax-1re 7429  ax-icn 7430  ax-addcl 7431  ax-addrcl 7432  ax-mulcl 7433  ax-addcom 7435  ax-addass 7437  ax-distr 7439  ax-i2m1 7440  ax-0lt1 7441  ax-0id 7443  ax-rnegex 7444  ax-cnre 7446  ax-pre-ltirr 7447  ax-pre-ltwlin 7448  ax-pre-lttrn 7449  ax-pre-ltadd 7451
This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3429  df-sn 3450  df-pr 3451  df-op 3453  df-uni 3652  df-int 3687  df-iun 3730  df-br 3844  df-opab 3898  df-mpt 3899  df-tr 3935  df-id 4118  df-iord 4191  df-on 4193  df-ilim 4194  df-suc 4196  df-iom 4404  df-xp 4442  df-rel 4443  df-cnv 4444  df-co 4445  df-dm 4446  df-rn 4447  df-res 4448  df-ima 4449  df-iota 4975  df-fun 5012  df-fn 5013  df-f 5014  df-f1 5015  df-fo 5016  df-f1o 5017  df-fv 5018  df-riota 5600  df-ov 5647  df-oprab 5648  df-mpt2 5649  df-1st 5903  df-2nd 5904  df-recs 6062  df-frec 6148  df-pnf 7514  df-mnf 7515  df-xr 7516  df-ltxr 7517  df-le 7518  df-sub 7645  df-neg 7646  df-inn 8413  df-n0 8664  df-z 8741  df-uz 9010  df-iseq 9841  df-seq3 9842
This theorem is referenced by:  seq3-1  9865  seqf  9868  seq3p1  9872
  Copyright terms: Public domain W3C validator