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 |-> <. (