ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  seqvalcd Unicode version
Theorem seqvalcd 10232
Description: Value of the sequence builder function. Similar to seq3val 10231 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 3119 . . . . . . 7 |- C C_ _V
43a1i 9 . . . . . 6 |- ( ph -> C C_ _V )
5 eqidd 2140 . . . . . . . 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 521 . . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) /\ ( z = x /\ w = y ) ) -> w = y )
7 simprl 520 . . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) /\ ( z = x /\ w = y ) ) -> z = x )
87fvoveq1d 5796 . . . . . . . . 9 |- ( ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) /\ ( z = x /\ w = y ) ) -> ( F ` ( z + 1 ) ) = ( F ` ( x + 1 ) ) )
96, 8oveq12d 5792 . . . . . . . 8 |- ( ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) /\ ( z = x /\ w = y ) ) -> ( w .+ ( F ` ( z + 1 ) ) ) = ( y .+ ( F ` ( x + 1 ) ) ) )
10 simprl 520 . . . . . . . 8 |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) -> x e. ( ZZ>= ` M ) )
11 simprr 521 . . . . . . . 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 2514 . . . . . . . . . . 11 |- ( ph -> A. x e. C A. y e. D ( x .+ y ) e. C )
14 oveq1 5781 . . . . . . . . . . . . 13 |- ( x = a -> ( x .+ y ) = ( a .+ y ) )
1514eleq1d 2208 . . . . . . . . . . . 12 |- ( x = a -> ( ( x .+ y ) e. C <-> ( a .+ y ) e. C ) )
16 oveq2 5782 . . . . . . . . . . . . 13 |- ( y = b -> ( a .+ y ) = ( a .+ b ) )
1716eleq1d 2208 . . . . . . . . . . . 12 |- ( y = b -> ( ( a .+ y ) e. C <-> ( a .+ b ) e. C ) )
1815, 17cbvral2v 2665 . . . . . . . . . . 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 274 . . . . . . . . 9 |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) -> A. a e. C A. b e. D ( a .+ b ) e. C )
21 fveq2 5421 . . . . . . . . . . . 12 |- ( a = ( x + 1 ) -> ( F ` a ) = ( F ` ( x + 1 ) ) )
2221eleq1d 2208 . . . . . . . . . . 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 2505 . . . . . . . . . . . . 13 |- ( ph -> A. x e. ( ZZ>= ` ( M + 1 ) ) ( F ` x ) e. D )
25 fveq2 5421 . . . . . . . . . . . . . . 15 |- ( x = a -> ( F ` x ) = ( F ` a ) )
2625eleq1d 2208 . . . . . . . . . . . . . 14 |- ( x = a -> ( ( F ` x ) e. D <-> ( F ` a ) e. D ) )
2726cbvralv 2654 . . . . . . . . . . . . 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 274 . . . . . . . . . . 11 |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) -> A. a e. ( ZZ>= ` ( M + 1 ) ) ( F ` a ) e. D )
30 eluzp1p1 9351 . . . . . . . . . . . 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 2794 . . . . . . . . . 10 |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) -> ( F ` ( x + 1 ) ) e. D )
33 oveq12 5783 . . . . . . . . . . . 12 |- ( ( a = y /\ b = ( F ` ( x + 1 ) ) ) -> ( a .+ b ) = ( y .+ ( F ` ( x + 1 ) ) ) )
3433eleq1d 2208 . . . . . . . . . . 11 |- ( ( a = y /\ b = ( F ` ( x + 1 ) ) ) -> ( ( a .+ b ) e. C <-> ( y .+ ( F ` ( x + 1 ) ) ) e. C ) )
3534rspc2gv 2801 . . . . . . . . . 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 408 . . . . . . . . 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 5898 . . . . . . 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 2216 . . . . . 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 10188 . . . . 5 |- ( ph -> R : om --> ( ( ZZ>= ` M ) X. C ) )
4241ffnd 5273 . . . 4 |- ( ph -> R Fn om )
43 1st2nd2 6073 . . . . . . . . . . . 12 |- ( u e. ( ( ZZ>= ` M ) X. C ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
4443adantl 275 . . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
4544fveq2d 5425 . . . . . . . . . 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 5777 . . . . . . . . . 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 2190 . . . . . . . . 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 6063 . . . . . . . . . . 11 |- ( u e. ( ( ZZ>= ` M ) X. C ) -> ( 1st ` u ) e. ( ZZ>= ` M ) )
4948adantl 275 . . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> ( 1st ` u ) e. ( ZZ>= ` M ) )
50 xp2nd 6064 . . . . . . . . . . . 12 |- ( u e. ( ( ZZ>= ` M ) X. C ) -> ( 2nd ` u ) e. C )
5150adantl 275 . . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> ( 2nd ` u ) e. C )
5251elexd 2699 . . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> ( 2nd ` u ) e. _V )
53 peano2uz 9378 . . . . . . . . . . . 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 274 . . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> A. x e. C A. y e. D ( x .+ y ) e. C )
56 fveq2 5421 . . . . . . . . . . . . . . 15 |- ( x = ( ( 1st ` u ) + 1 ) -> ( F ` x ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
5756eleq1d 2208 . . . . . . . . . . . . . 14 |- ( x = ( ( 1st ` u ) + 1 ) -> ( ( F ` x ) e. D <-> ( F ` ( ( 1st ` u ) + 1 ) ) e. D ) )
5824adantr 274 . . . . . . . . . . . . . 14 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> A. x e. ( ZZ>= ` ( M + 1 ) ) ( F ` x ) e. D )
59 eluzp1p1 9351 . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> ( F ` ( ( 1st ` u ) + 1 ) ) e. D )
62 oveq12 5783 . . . . . . . . . . . . . . 15 |- ( ( x = ( 2nd ` u ) /\ y = ( F ` ( ( 1st ` u ) + 1 ) ) ) -> ( x .+ y ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
6362eleq1d 2208 . . . . . . . . . . . . . 14 |- ( ( x = ( 2nd ` u ) /\ y = ( F ` ( ( 1st ` u ) + 1 ) ) ) -> ( ( x .+ y ) e. C <-> ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) e. C ) )
6463rspc2gv 2801 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 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 4572 . . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. C ) ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. C ) )
68 oveq1 5781 . . . . . . . . . . . 12 |- ( x = ( 1st ` u ) -> ( x + 1 ) = ( ( 1st ` u ) + 1 ) )
69 fvoveq1 5797 . . . . . . . . . . . . 13 |- ( x = ( 1st ` u ) -> ( F ` ( x + 1 ) ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
7069oveq2d 5790 . . . . . . . . . . . 12 |- ( x = ( 1st ` u ) -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
7168, 70opeq12d 3713 . . . . . . . . . . 11 |- ( x = ( 1st ` u ) -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( ( 1st ` u ) + 1 ) , ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
72 oveq1 5781 . . . . . . . . . . . 12 |- ( y = ( 2nd ` u ) -> ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
7372opeq2d 3712 . . . . . . . . . . 11 |- ( y = ( 2nd ` u ) -> <. ( ( 1st ` u ) + 1 ) , ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. = <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
74 eqid 2139 . . . . . . . . . . 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 5905 . . . . . . . . . 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 1216 . . . . . . . . 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 2172 . . . . . . . 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 2216 . . . . . . 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 2505 . . . . . 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 9340 . . . . . . . 8 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
811, 80syl 14 . . . . . . 7 |- ( ph -> M e. ( ZZ>= ` M ) )
8281, 2opelxpd 4572 . . . . . 6 |- ( ph -> <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. C ) )
8379, 82jca 304 . . . . 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 6302 . . . . 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 5272 . . . . 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 5421 . . . . . . . 8 |- ( c = (/) -> ( R ` c ) = ( R ` (/) ) )
88 fveq2 5421 . . . . . . . 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 2154 . . . . . . 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 5421 . . . . . . . 8 |- ( c = k -> ( R ` c ) = ( R ` k ) )
92 fveq2 5421 . . . . . . . 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 2154 . . . . . . 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 5421 . . . . . . . 8 |- ( c = suc k -> ( R ` c ) = ( R ` suc k ) )
96 fveq2 5421 . . . . . . . 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 2154 . . . . . . 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 5421 . . . . . . . 8 |- ( c = n -> ( R ` c ) = ( R ` n ) )
100 fveq2 5421 . . . . . . . 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 2154 . . . . . . 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 5422 . . . . . . . 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 6294 . . . . . . . . 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 2184 . . . . . . 7 |- ( ph -> ( R ` (/) ) = <. M , ( F ` M ) >. )
107 frec0g 6294 . . . . . . . 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 2175 . . . . . 6 |- ( ph -> ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) )
11041ad2antlr 480 . . . . . . . . . . . 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 518 . . . . . . . . . . . 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 5556 . . . . . . . . . . 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 6063 . . . . . . . . . . 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 6064 . . . . . . . . . . . 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 2699 . . . . . . . . . 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 9378 . . . . . . . . . . . 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 480 . . . . . . . . . . . 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 5421 . . . . . . . . . . . . . . 15 |- ( a = ( ( 1st ` ( R ` k ) ) + 1 ) -> ( F ` a ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
122121eleq1d 2208 . . . . . . . . . . . . . 14 |- ( a = ( ( 1st ` ( R ` k ) ) + 1 ) -> ( ( F ` a ) e. D <-> ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) e. D ) )
12328ad2antlr 480 . . . . . . . . . . . . . 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 9351 . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . 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 5783 . . . . . . . . . . . . . . 15 |- ( ( x = ( 2nd ` ( R ` k ) ) /\ y = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) -> ( x .+ y ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
128127eleq1d 2208 . . . . . . . . . . . . . 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 2801 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 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 4572 . . . . . . . . . 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 5781 . . . . . . . . . . . 12 |- ( x = ( 1st ` ( R ` k ) ) -> ( x + 1 ) = ( ( 1st ` ( R ` k ) ) + 1 ) )
134 fvoveq1 5797 . . . . . . . . . . . . 13 |- ( x = ( 1st ` ( R ` k ) ) -> ( F ` ( x + 1 ) ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
135134oveq2d 5790 . . . . . . . . . . . 12 |- ( x = ( 1st ` ( R ` k ) ) -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
136133, 135opeq12d 3713 . . . . . . . . . . 11 |- ( x = ( 1st ` ( R ` k ) ) -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
137 oveq1 5781 . . . . . . . . . . . 12 |- ( y = ( 2nd ` ( R ` k ) ) -> ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
138137opeq2d 3712 . . . . . . . . . . 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 5905 . . . . . . . . . 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 1216 . . . . . . . . 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 480 . . . . . . . . . . 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 480 . . . . . . . . . . 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 6304 . . . . . . . . . . 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 1216 . . . . . . . . . 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 5425 . . . . . . . . . 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 6073 . . . . . . . . . . . . 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 5425 . . . . . . . . . . 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 5777 . . . . . . . . . . 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 2190 . . . . . . . . . 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 2178 . . . . . . . . 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 5425 . . . . . . . . . . . . . . . . . . 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 5777 . . . . . . . . . . . . . . . . . . 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 2190 . . . . . . . . . . . . . . . . . 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 5797 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = ( 1st ` u ) -> ( F ` ( z + 1 ) ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
157156oveq2d 5790 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( z = ( 1st ` u ) -> ( w .+ ( F ` ( z + 1 ) ) ) = ( w .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
158 oveq1 5781 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = ( 2nd ` u ) -> ( w .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
159 eqid 2139 . . . . . . . . . . . . . . . . . . . . . . 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 5905 . . . . . . . . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . . . . . . . . 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 2216 . . . . . . . . . . . . . . . . . . . 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 4572 . . . . . . . . . . . . . . . . . . 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 5781 . . . . . . . . . . . . . . . . . . . . 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 3713 . . . . . . . . . . . . . . . . . . . 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 5782 . . . . . . . . . . . . . . . . . . . . 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 3712 . . . . . . . . . . . . . . . . . . . 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 2139 . . . . . . . . . . . . . . . . . . . 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 5905 . . . . . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . . . . . 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 2172 . . . . . . . . . . . . . . . . 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 2216 . . . . . . . . . . . . . . . 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 2505 . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . 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 6304 . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . 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 5422 . . . . . . . . . . . . 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 5422 . . . . . . . . . . . . . 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 5424 . . . . . . . . . . . . 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 2197 . . . . . . . . . . . 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 5425 . . . . . . . . . . . 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 2172 . . . . . . . . . . 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 5777 . . . . . . . . . . 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 2190 . . . . . . . . . 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 5797 . . . . . . . . . . . . . . . 16 |- ( z = ( 1st ` ( R ` k ) ) -> ( F ` ( z + 1 ) ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
186185oveq2d 5790 . . . . . . . . . . . . . . 15 |- ( z = ( 1st ` ( R ` k ) ) -> ( w .+ ( F ` ( z + 1 ) ) ) = ( w .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
187 oveq1 5781 . . . . . . . . . . . . . . 15 |- ( w = ( 2nd ` ( R ` k ) ) -> ( w .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
188186, 187, 159ovmpog 5905 . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . 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 2216 . . . . . . . . . . . 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 4572 . . . . . . . . . . 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 5781 . . . . . . . . . . . . 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 3713 . . . . . . . . . . . 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 5782 . . . . . . . . . . . . 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 3712 . . . . . . . . . . . 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 5905 . . . . . . . . . . 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 1216 . . . . . . . . . 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 3712 . . . . . . . . . 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 2176 . . . . . . . . 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 2183 . . . . . . . 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 361 . . . . . . 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 4514 . . . . 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 5521 . . 3 |- ( ph -> R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
206205rneqd 4768 . 2 |- ( ph -> ran R = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
207 df-seqfrec 10219 . 2 |- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
208206, 207syl6reqr 2191 1 |- ( ph -> seq M ( .+ , F ) = ran R )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331   e. wcel 1480   A.wral 2416   _Vcvv 2686   C_ wss 3071   (/)c0 3363   <.cop 3530   suc csuc 4287   omcom 4504   X. cxp 4537   ran crn 4540   Fn wfn 5118   -->wf 5119   ` cfv 5123  (class class class)co 5774   e. cmpo 5776   1stc1st 6036   2ndc2nd 6037  freccfrec 6287   1c1 7621   + caddc 7623   ZZcz 9054   ZZ>=cuz 9326   seqcseq 10218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-addcom 7720  ax-addass 7722  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-0id 7728  ax-rnegex 7729  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-ltadd 7736
This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-inn 8721  df-n0 8978  df-z 9055  df-uz 9327  df-seqfrec 10219
This theorem is referenced by:  seqf2  10237  seq1cd  10238  seqp1cd  10239
  Copyright terms: Public domain W3C validator