Theorem seq3val 9862

Description: Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 9868, seq3-1 9865 and seq3p1 9872, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.)

Hypotheses

Ref	Expression
seq3val.m	|- ( ph -> M e. ZZ )
seq3val.r	|- R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. )
seq3val.f	|- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )
seq3val.pl	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )

Assertion

Ref	Expression
seq3val	|- ( ph -> seq M ( .+ , F ) = ran R )

Distinct variable groups:   x, .+ , y, w, z   x, F, y, w, z   x, M, y, w, z   x, R, y, w, z   x, S, y, w, z   ph, x, y, w, z

Proof of Theorem seq3val

Dummy variables a b k c n u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		seq3val.m	. . . . . 6 |- ( ph -> M e. ZZ )
2		fveq2 5299	. . . . . . . 8 |- ( x = M -> ( F ` x ) = ( F ` M ) )
3	2	eleq1d 2156	. . . . . . 7 |- ( x = M -> ( ( F ` x ) e. S <-> ( F ` M ) e. S ) )
4		seq3val.f	. . . . . . . 8 |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )
5	4	ralrimiva 2446	. . . . . . 7 |- ( ph -> A. x e. ( ZZ>= ` M ) ( F ` x ) e. S )
6		uzid 9023	. . . . . . . 8 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
7	1, 6	syl 14	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` M ) )
8	3, 5, 7	rspcdva 2727	. . . . . 6 |- ( ph -> ( F ` M ) e. S )
9		ssv 3046	. . . . . . 7 |- S C_ _V
10	9	a1i 9	. . . . . 6 |- ( ph -> S C_ _V )
11		seq3val.pl	. . . . . . 7 |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
12	4, 11	iseqovex 9858	. . . . . 6 |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. S ) ) -> ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) e. S )
13		seq3val.r	. . . . . 6 |- R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. )
14	1, 8, 10, 12, 13	frecuzrdgrclt 9810	. . . . 5 |- ( ph -> R : om --> ( ( ZZ>= ` M ) X. S ) )
15		ffn 5155	. . . . 5 |- ( R : om --> ( ( ZZ>= ` M ) X. S ) -> R Fn om )
16	14, 15	syl 14	. . . 4 |- ( ph -> R Fn om )
17		1st2nd2 5937	. . . . . . . . . . . 12 |- ( u e. ( ( ZZ>= ` M ) X. S ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
18	17	adantl 271	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> u = <. ( 1st ` u ) , ( 2nd ` u ) >. )
19	18	fveq2d 5303	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` <. ( 1st ` u ) , ( 2nd ` u ) >. ) )
20		df-ov 5647	. . . . . . . . . 10 |- ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` u ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` <. ( 1st ` u ) , ( 2nd ` u ) >. )
21	19, 20	syl6eqr 2138	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) = ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` u ) ) )
22		xp1st 5928	. . . . . . . . . . 11 |- ( u e. ( ( ZZ>= ` M ) X. S ) -> ( 1st ` u ) e. ( ZZ>= ` M ) )
23	22	adantl 271	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( 1st ` u ) e. ( ZZ>= ` M ) )
24		xp2nd 5929	. . . . . . . . . . . 12 |- ( u e. ( ( ZZ>= ` M ) X. S ) -> ( 2nd ` u ) e. S )
25	24	adantl 271	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( 2nd ` u ) e. S )
26	25	elexd 2632	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( 2nd ` u ) e. _V )
27		peano2uz 9061	. . . . . . . . . . . 12 |- ( ( 1st ` u ) e. ( ZZ>= ` M ) -> ( ( 1st ` u ) + 1 ) e. ( ZZ>= ` M ) )
28	23, 27	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) + 1 ) e. ( ZZ>= ` M ) )
29	11	caovclg 5789	. . . . . . . . . . . . 13 |- ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a .+ b ) e. S )
30	29	adantlr 461	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) /\ ( a e. S /\ b e. S ) ) -> ( a .+ b ) e. S )
31		fveq2 5299	. . . . . . . . . . . . . 14 |- ( x = ( ( 1st ` u ) + 1 ) -> ( F ` x ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
32	31	eleq1d 2156	. . . . . . . . . . . . 13 |- ( x = ( ( 1st ` u ) + 1 ) -> ( ( F ` x ) e. S <-> ( F ` ( ( 1st ` u ) + 1 ) ) e. S ) )
33	5	adantr 270	. . . . . . . . . . . . 13 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> A. x e. ( ZZ>= ` M ) ( F ` x ) e. S )
34	32, 33, 28	rspcdva 2727	. . . . . . . . . . . 12 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( F ` ( ( 1st ` u ) + 1 ) ) e. S )
35	30, 25, 34	caovcld 5790	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) e. S )
36		opelxpi 4467	. . . . . . . . . . 11 |- ( ( ( ( 1st ` u ) + 1 ) e. ( ZZ>= ` M ) /\ ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) e. S ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
37	28, 35, 36	syl2anc 403	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
38		oveq1 5651	. . . . . . . . . . . 12 |- ( x = ( 1st ` u ) -> ( x + 1 ) = ( ( 1st ` u ) + 1 ) )
39		fvoveq1 5667	. . . . . . . . . . . . 13 |- ( x = ( 1st ` u ) -> ( F ` ( x + 1 ) ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
40	39	oveq2d 5660	. . . . . . . . . . . 12 |- ( x = ( 1st ` u ) -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
41	38, 40	opeq12d 3628	. . . . . . . . . . 11 |- ( x = ( 1st ` u ) -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( ( 1st ` u ) + 1 ) , ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
42		oveq1 5651	. . . . . . . . . . . 12 |- ( y = ( 2nd ` u ) -> ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
43	42	opeq2d 3627	. . . . . . . . . . 11 |- ( y = ( 2nd ` u ) -> <. ( ( 1st ` u ) + 1 ) , ( y .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. = <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
44		eqid 2088	. . . . . . . . . . 11 |- ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) = ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. )
45	41, 43, 44	ovmpt2g 5771	. . . . . . . . . 10 |- ( ( ( 1st ` u ) e. ( ZZ>= ` M ) /\ ( 2nd ` u ) e. _V /\ <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` u ) ) = <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
46	23, 26, 37, 45	syl3anc 1174	. . . . . . . . 9 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` u ) ) = <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
47	21, 46	eqtrd 2120	. . . . . . . 8 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) = <. ( ( 1st ` u ) + 1 ) , ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) >. )
48	47, 37	eqeltrd 2164	. . . . . . 7 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
49	48	ralrimiva 2446	. . . . . 6 |- ( ph -> A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
50		opelxpi 4467	. . . . . . 7 |- ( ( M e. ( ZZ>= ` M ) /\ ( F ` M ) e. S ) -> <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) )
51	7, 8, 50	syl2anc 403	. . . . . 6 |- ( ph -> <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) )
52	49, 51	jca 300	. . . . 5 |- ( ph -> ( A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) /\ <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) ) )
53		frecfcl 6162	. . . . 5 |- ( ( A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) /\ <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) ) -> frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) : om --> ( ( ZZ>= ` M ) X. S ) )
54		ffn 5155	. . . . 5 |- (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) : om --> ( ( ZZ>= ` M ) X. S ) -> frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) Fn om )
55	52, 53, 54	3syl 17	. . . 4 |- ( ph -> frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) Fn om )
56		fveq2 5299	. . . . . . . 8 |- ( c = (/) -> ( R ` c ) = ( R ` (/) ) )
57		fveq2 5299	. . . . . . . 8 |- ( c = (/) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) )
58	56, 57	eqeq12d 2102	. . . . . . 7 |- ( c = (/) -> ( ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) <-> ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) ) )
59	58	imbi2d 228	. . . . . 6 |- ( c = (/) -> ( ( ph -> ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) ) <-> ( ph -> ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) ) ) )
60		fveq2 5299	. . . . . . . 8 |- ( c = k -> ( R ` c ) = ( R ` k ) )
61		fveq2 5299	. . . . . . . 8 |- ( c = k -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) )
62	60, 61	eqeq12d 2102	. . . . . . 7 |- ( c = k -> ( ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) <-> ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
63	62	imbi2d 228	. . . . . 6 |- ( c = k -> ( ( ph -> ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) ) <-> ( ph -> ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) ) )
64		fveq2 5299	. . . . . . . 8 |- ( c = suc k -> ( R ` c ) = ( R ` suc k ) )
65		fveq2 5299	. . . . . . . 8 |- ( c = suc k -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) )
66	64, 65	eqeq12d 2102	. . . . . . 7 |- ( c = suc k -> ( ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) <-> ( R ` suc k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) ) )
67	66	imbi2d 228	. . . . . 6 |- ( c = suc k -> ( ( ph -> ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) ) <-> ( ph -> ( R ` suc k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) ) ) )
68		fveq2 5299	. . . . . . . 8 |- ( c = n -> ( R ` c ) = ( R ` n ) )
69		fveq2 5299	. . . . . . . 8 |- ( c = n -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` n ) )
70	68, 69	eqeq12d 2102	. . . . . . 7 |- ( c = n -> ( ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) <-> ( R ` n ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` n ) ) )
71	70	imbi2d 228	. . . . . 6 |- ( c = n -> ( ( ph -> ( R ` c ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` c ) ) <-> ( ph -> ( R ` n ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` n ) ) ) )
72	13	fveq1i 5300	. . . . . . . 8 |- ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` (/) )
73		frec0g 6154	. . . . . . . . 9 |- ( <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) = <. M , ( F ` M ) >. )
74	51, 73	syl 14	. . . . . . . 8 |- ( ph -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) = <. M , ( F ` M ) >. )
75	72, 74	syl5eq 2132	. . . . . . 7 |- ( ph -> ( R ` (/) ) = <. M , ( F ` M ) >. )
76		frec0g 6154	. . . . . . . 8 |- ( <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) = <. M , ( F ` M ) >. )
77	51, 76	syl 14	. . . . . . 7 |- ( ph -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) = <. M , ( F ` M ) >. )
78	75, 77	eqtr4d 2123	. . . . . 6 |- ( ph -> ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` (/) ) )
79	14	ad2antlr 473	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> R : om --> ( ( ZZ>= ` M ) X. S ) )
80		simpll 496	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> k e. om )
81	79, 80	ffvelrnd 5429	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` k ) e. ( ( ZZ>= ` M ) X. S ) )
82		xp1st 5928	. . . . . . . . . . 11 |- ( ( R ` k ) e. ( ( ZZ>= ` M ) X. S ) -> ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) )
83	81, 82	syl 14	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) )
84		xp2nd 5929	. . . . . . . . . . . 12 |- ( ( R ` k ) e. ( ( ZZ>= ` M ) X. S ) -> ( 2nd ` ( R ` k ) ) e. S )
85	81, 84	syl 14	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( 2nd ` ( R ` k ) ) e. S )
86	85	elexd 2632	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( 2nd ` ( R ` k ) ) e. _V )
87	29	adantll 460	. . . . . . . . . . . . . . 15 |- ( ( ( k e. om /\ ph ) /\ ( a e. S /\ b e. S ) ) -> ( a .+ b ) e. S )
88	87	adantlr 461	. . . . . . . . . . . . . 14 |- ( ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) /\ ( a e. S /\ b e. S ) ) -> ( a .+ b ) e. S )
89		fveq2 5299	. . . . . . . . . . . . . . . 16 |- ( a = ( ( 1st ` ( R ` k ) ) + 1 ) -> ( F ` a ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
90	89	eleq1d 2156	. . . . . . . . . . . . . . 15 |- ( a = ( ( 1st ` ( R ` k ) ) + 1 ) -> ( ( F ` a ) e. S <-> ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) e. S ) )
91		fveq2 5299	. . . . . . . . . . . . . . . . . . 19 |- ( x = a -> ( F ` x ) = ( F ` a ) )
92	91	eleq1d 2156	. . . . . . . . . . . . . . . . . 18 |- ( x = a -> ( ( F ` x ) e. S <-> ( F ` a ) e. S ) )
93	92	cbvralv 2590	. . . . . . . . . . . . . . . . 17 |- ( A. x e. ( ZZ>= ` M ) ( F ` x ) e. S <-> A. a e. ( ZZ>= ` M ) ( F ` a ) e. S )
94	5, 93	sylib 120	. . . . . . . . . . . . . . . 16 |- ( ph -> A. a e. ( ZZ>= ` M ) ( F ` a ) e. S )
95	94	ad2antlr 473	. . . . . . . . . . . . . . 15 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> A. a e. ( ZZ>= ` M ) ( F ` a ) e. S )
96		peano2uz 9061	. . . . . . . . . . . . . . . 16 |- ( ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) -> ( ( 1st ` ( R ` k ) ) + 1 ) e. ( ZZ>= ` M ) )
97	83, 96	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 1st ` ( R ` k ) ) + 1 ) e. ( ZZ>= ` M ) )
98	90, 95, 97	rspcdva 2727	. . . . . . . . . . . . . 14 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) e. S )
99	88, 85, 98	caovcld 5790	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) e. S )
100		fvoveq1 5667	. . . . . . . . . . . . . . 15 |- ( z = ( 1st ` ( R ` k ) ) -> ( F ` ( z + 1 ) ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
101	100	oveq2d 5660	. . . . . . . . . . . . . 14 |- ( z = ( 1st ` ( R ` k ) ) -> ( w .+ ( F ` ( z + 1 ) ) ) = ( w .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
102		oveq1 5651	. . . . . . . . . . . . . 14 |- ( w = ( 2nd ` ( R ` k ) ) -> ( w .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
103		eqid 2088	. . . . . . . . . . . . . 14 |- ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) = ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) )
104	101, 102, 103	ovmpt2g 5771	. . . . . . . . . . . . 13 |- ( ( ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) /\ ( 2nd ` ( R ` k ) ) e. S /\ ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) e. S ) -> ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
105	83, 85, 99, 104	syl3anc 1174	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
106	105	opeq2d 3627	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
107	105, 99	eqeltrd 2164	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) e. S )
108		opelxpi 4467	. . . . . . . . . . . 12 |- ( ( ( ( 1st ` ( R ` k ) ) + 1 ) e. ( ZZ>= ` M ) /\ ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) e. S ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
109	97, 107, 108	syl2anc 403	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
110	106, 109	eqeltrrd 2165	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
111		oveq1 5651	. . . . . . . . . . . 12 |- ( x = ( 1st ` ( R ` k ) ) -> ( x + 1 ) = ( ( 1st ` ( R ` k ) ) + 1 ) )
112		fvoveq1 5667	. . . . . . . . . . . . 13 |- ( x = ( 1st ` ( R ` k ) ) -> ( F ` ( x + 1 ) ) = ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) )
113	112	oveq2d 5660	. . . . . . . . . . . 12 |- ( x = ( 1st ` ( R ` k ) ) -> ( y .+ ( F ` ( x + 1 ) ) ) = ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
114	111, 113	opeq12d 3628	. . . . . . . . . . 11 |- ( x = ( 1st ` ( R ` k ) ) -> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
115		oveq1 5651	. . . . . . . . . . . 12 |- ( y = ( 2nd ` ( R ` k ) ) -> ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) = ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) )
116	115	opeq2d 3627	. . . . . . . . . . 11 |- ( y = ( 2nd ` ( R ` k ) ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( y .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
117	114, 116, 44	ovmpt2g 5771	. . . . . . . . . 10 |- ( ( ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) /\ ( 2nd ` ( R ` k ) ) e. _V /\ <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` ( R ` k ) ) ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
118	83, 86, 110, 117	syl3anc 1174	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` ( R ` k ) ) ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
119	49	ad2antlr 473	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
120	51	ad2antlr 473	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) )
121		frecsuc 6164	. . . . . . . . . . . 12 |- ( ( A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) /\ <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) /\ k e. om ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
122	119, 120, 80, 121	syl3anc 1174	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
123		simpr 108	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) )
124	123	fveq2d 5303	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` ( R ` k ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
125	122, 124	eqtr4d 2123	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` ( R ` k ) ) )
126		1st2nd2 5937	. . . . . . . . . . . . 13 |- ( ( R ` k ) e. ( ( ZZ>= ` M ) X. S ) -> ( R ` k ) = <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. )
127	81, 126	syl 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 ) ) >. )
128	127	fveq2d 5303	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` ( R ` k ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. ) )
129		df-ov 5647	. . . . . . . . . . 11 |- ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` ( R ` k ) ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. )
130	128, 129	syl6eqr 2138	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ` ( R ` k ) ) = ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` ( R ` k ) ) ) )
131	125, 130	eqtrd 2120	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) ( 2nd ` ( R ` k ) ) ) )
132	13	fveq1i 5300	. . . . . . . . . . . . . . 15 |- ( R ` suc k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` suc k )
133	18	fveq2d 5303	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` <. ( 1st ` u ) , ( 2nd ` u ) >. ) )
134		df-ov 5647	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` u ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` <. ( 1st ` u ) , ( 2nd ` u ) >. )
135	133, 134	syl6eqr 2138	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) = ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` u ) ) )
136		fvoveq1 5667	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = ( 1st ` u ) -> ( F ` ( z + 1 ) ) = ( F ` ( ( 1st ` u ) + 1 ) ) )
137	136	oveq2d 5660	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = ( 1st ` u ) -> ( w .+ ( F ` ( z + 1 ) ) ) = ( w .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
138		oveq1 5651	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( w = ( 2nd ` u ) -> ( w .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
139	137, 138, 103	ovmpt2g 5771	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( 1st ` u ) e. ( ZZ>= ` M ) /\ ( 2nd ` u ) e. S /\ ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) e. S ) -> ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
140	23, 25, 35, 139	syl3anc 1174	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) = ( ( 2nd ` u ) .+ ( F ` ( ( 1st ` u ) + 1 ) ) ) )
141	140, 35	eqeltrd 2164	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) e. S )
142		opelxpi 4467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 1st ` u ) + 1 ) e. ( ZZ>= ` M ) /\ ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) e. S ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
143	28, 141, 142	syl2anc 403	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. e. ( ( ZZ>= ` M ) X. S ) )
144		oveq1 5651	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = ( 1st ` u ) -> ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) )
145	38, 144	opeq12d 3628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = ( 1st ` u ) -> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. = <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. )
146		oveq2 5652	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = ( 2nd ` u ) -> ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) )
147	146	opeq2d 3627	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( 2nd ` u ) -> <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. = <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. )
148		eqid 2088	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) = ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. )
149	145, 147, 148	ovmpt2g 5771	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 1st ` u ) e. ( ZZ>= ` M ) /\ ( 2nd ` u ) e. _V /\ <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` u ) ) = <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. )
150	23, 26, 143, 149	syl3anc 1174	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` u ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` u ) ) = <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. )
151	135, 150	eqtrd 2120	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) = <. ( ( 1st ` u ) + 1 ) , ( ( 1st ` u ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` u ) ) >. )
152	151, 143	eqeltrd 2164	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ u e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
153	152	ralrimiva 2446	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
154	153	ad2antlr 473	. . . . . . . . . . . . . . . 16 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) )
155		frecsuc 6164	. . . . . . . . . . . . . . . 16 |- ( ( A. u e. ( ( ZZ>= ` M ) X. S ) ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` u ) e. ( ( ZZ>= ` M ) X. S ) /\ <. M , ( F ` M ) >. e. ( ( ZZ>= ` M ) X. S ) /\ k e. om ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
156	154, 120, 80, 155	syl3anc 1174	. . . . . . . . . . . . . . 15 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
157	132, 156	syl5eq 2132	. . . . . . . . . . . . . 14 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) )
158	13	fveq1i 5300	. . . . . . . . . . . . . . 15 |- ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` k )
159	158	fveq2i 5302	. . . . . . . . . . . . . 14 |- ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` ( R ` k ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) ` k ) )
160	157, 159	syl6eqr 2138	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` ( R ` k ) ) )
161	127	fveq2d 5303	. . . . . . . . . . . . 13 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` ( R ` k ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. ) )
162	160, 161	eqtrd 2120	. . . . . . . . . . . 12 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. ) )
163		df-ov 5647	. . . . . . . . . . . 12 |- ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` ( R ` k ) ) ) = ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ` <. ( 1st ` ( R ` k ) ) , ( 2nd ` ( R ` k ) ) >. )
164	162, 163	syl6eqr 2138	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` ( R ` k ) ) ) )
165		oveq1 5651	. . . . . . . . . . . . . 14 |- ( x = ( 1st ` ( R ` k ) ) -> ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) )
166	111, 165	opeq12d 3628	. . . . . . . . . . . . 13 |- ( x = ( 1st ` ( R ` k ) ) -> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. )
167		oveq2 5652	. . . . . . . . . . . . . 14 |- ( y = ( 2nd ` ( R ` k ) ) -> ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) = ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) )
168	167	opeq2d 3627	. . . . . . . . . . . . 13 |- ( y = ( 2nd ` ( R ` k ) ) -> <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. )
169	166, 168, 148	ovmpt2g 5771	. . . . . . . . . . . 12 |- ( ( ( 1st ` ( R ` k ) ) e. ( ZZ>= ` M ) /\ ( 2nd ` ( R ` k ) ) e. _V /\ <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. e. ( ( ZZ>= ` M ) X. S ) ) -> ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` ( R ` k ) ) ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. )
170	83, 86, 109, 169	syl3anc 1174	. . . . . . . . . . 11 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( ( 1st ` ( R ` k ) ) ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) ( 2nd ` ( R ` k ) ) ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. )
171	164, 170	eqtrd 2120	. . . . . . . . . 10 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 1st ` ( R ` k ) ) ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) ( 2nd ` ( R ` k ) ) ) >. )
172	171, 106	eqtrd 2120	. . . . . . . . 9 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = <. ( ( 1st ` ( R ` k ) ) + 1 ) , ( ( 2nd ` ( R ` k ) ) .+ ( F ` ( ( 1st ` ( R ` k ) ) + 1 ) ) ) >. )
173	118, 131, 172	3eqtr4rd 2131	. . . . . . . 8 |- ( ( ( k e. om /\ ph ) /\ ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) ) -> ( R ` suc k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) )
174	173	exp31 356	. . . . . . 7 |- ( k e. om -> ( ph -> ( ( R ` k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` k ) -> ( R ` suc k ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` suc k ) ) ) )
175	174	a2d 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 ) ) ) )
176	59, 63, 67, 71, 78, 175	finds 4413	. . . . 5 |- ( n e. om -> ( ph -> ( R ` n ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` n ) ) )
177	176	impcom 123	. . . 4 |- ( ( ph /\ n e. om ) -> ( R ` n ) = (frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) ` n ) )
178	16, 55, 177	eqfnfvd 5394	. . 3 |- ( ph -> R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
179	178	rneqd 4660	. 2 |- ( ph -> ran R = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. ) )
180		dfseq3-2 9843	. 2 |- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
181	179, 180	syl6reqr 2139	1 |- ( ph -> seq M ( .+ , F ) = ran R )

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   e. wcel 1438   A.wral 2359   _Vcvv 2619   C_ wss 2999   (/)c0 3286   <.cop 3447   suc csuc 4190   omcom 4403   X. cxp 4434   ran crn 4437   Fn wfn 5005   -->wf 5006   ` cfv 5010  (class class class)co 5644   |-> cmpt2 5646   1stc1st 5901   2ndc2nd 5902  freccfrec 6147   1c1 7341   + caddc 7343   ZZcz 8740   ZZ>=cuz 9009   seqcseq 9840

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3952  ax-sep 3955  ax-nul 3963  ax-pow 4007  ax-pr 4034  ax-un 4258  ax-setind 4351  ax-iinf 4401  ax-cnex 7426  ax-resscn 7427  ax-1cn 7428  ax-1re 7429  ax-icn 7430  ax-addcl 7431  ax-addrcl 7432  ax-mulcl 7433  ax-addcom 7435  ax-addass 7437  ax-distr 7439  ax-i2m1 7440  ax-0lt1 7441  ax-0id 7443  ax-rnegex 7444  ax-cnre 7446  ax-pre-ltirr 7447  ax-pre-ltwlin 7448  ax-pre-lttrn 7449  ax-pre-ltadd 7451

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3429  df-sn 3450  df-pr 3451  df-op 3453  df-uni 3652  df-int 3687  df-iun 3730  df-br 3844  df-opab 3898  df-mpt 3899  df-tr 3935  df-id 4118  df-iord 4191  df-on 4193  df-ilim 4194  df-suc 4196  df-iom 4404  df-xp 4442  df-rel 4443  df-cnv 4444  df-co 4445  df-dm 4446  df-rn 4447  df-res 4448  df-ima 4449  df-iota 4975  df-fun 5012  df-fn 5013  df-f 5014  df-f1 5015  df-fo 5016  df-f1o 5017  df-fv 5018  df-riota 5600  df-ov 5647  df-oprab 5648  df-mpt2 5649  df-1st 5903  df-2nd 5904  df-recs 6062  df-frec 6148  df-pnf 7514  df-mnf 7515  df-xr 7516  df-ltxr 7517  df-le 7518  df-sub 7645  df-neg 7646  df-inn 8413  df-n0 8664  df-z 8741  df-uz 9010  df-iseq 9841  df-seq3 9842

This theorem is referenced by:  seq3-1  9865  seqf  9868  seq3p1  9872