Theorem seq1suclem 6261

Description: Lemma for seq1p1 6263.

Hypotheses

Ref	Expression
seq1val.1	|- S e. V
seq1val.2	|- F e. V
seq1val.3	|- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
seq1val.4	|- H = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}

Assertion

Ref	Expression
seq1suclem	|- (A e. NN -> ((S seq1 F)` (A + 1)) = (((S seq1 F)` A)S(F` (A + 1))))

Distinct variable groups:   z,w,F   z,S,w

Proof of Theorem seq1suclem

Step	Hyp	Ref	Expression
1		nnzrab 6112	. . . . . . . 8 |- NN = {x e. ZZ | 1 <_ x}
2	1	eleq2i 1535	. . . . . . 7 |- (A e. NN <-> A e. {x e. ZZ | 1 <_ x})
3		1z 6114	. . . . . . . 8 |- 1 e. ZZ
4		seq1val.3	. . . . . . . 8 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
5	3, 4	uzrdgsuc 6249	. . . . . . 7 |- (A e. {x e. ZZ | 1 <_ x} -> ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1)) = (H` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)))
6	2, 5	sylbi 199	. . . . . 6 |- (A e. NN -> ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1)) = (H` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)))
7		seq1val.4	. . . . . . . 8 |- H = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}
8		fveq2 3715	. . . . . . . . . . . . 13 |- (x = z -> (1st` x) = (1st` z))
9	8	opreq1d 3966	. . . . . . . . . . . 12 |- (x = z -> ((1st` x) + 1) = ((1st` z) + 1))
10		fveq2 3715	. . . . . . . . . . . . 13 |- (x = z -> (2nd` x) = (2nd` z))
11	9	fveq2d 3719	. . . . . . . . . . . . 13 |- (x = z -> (F` ((1st` x) + 1)) = (F` ((1st` z) + 1)))
12	10, 11	opreq12d 3969	. . . . . . . . . . . 12 |- (x = z -> ((2nd` x)S(F` ((1st` x) + 1))) = ((2nd` z)S(F` ((1st` z) + 1))))
13	9, 12	opeq12d 2491	. . . . . . . . . . 11 |- (x = z -> <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.)
14	13	eqeq2d 1483	. . . . . . . . . 10 |- (x = z -> (y = <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>. <-> y = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.))
15		eqeq1 1478	. . . . . . . . . 10 |- (y = w -> (y = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>. <-> w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.))
16	14, 15	sylan9bb 539	. . . . . . . . 9 |- ((x = z /\ y = w) -> (y = <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>. <-> w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.))
17	16	cbvopabv 2668	. . . . . . . 8 |- {<.x, y>. | y = <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>.} = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}
18	7, 17	eqtr4 1495	. . . . . . 7 |- H = {<.x, y>. | y = <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>.}
19		fvex 3723	. . . . . . 7 |- ((rec(H, <.1, (F` 1)>.) o. `'G)` A) e. V
20	18, 19	seq1rval 6256	. . . . . 6 |- (H` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) = <.((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1), ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1)))>.
21	6, 20	syl6eq 1520	. . . . 5 |- (A e. NN -> ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1)) = <.((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1), ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1)))>.)
22	21	fveq2d 3719	. . . 4 |- (A e. NN -> (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1))) = (2nd` <.((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1), ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1)))>.))
23		oprex 3974	. . . . 5 |- ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1) e. V
24		oprex 3974	. . . . 5 |- ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1))) e. V
25	23, 24	op2nd 4076	. . . 4 |- (2nd` <.((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1), ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1)))>.) = ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1)))
26	22, 25	syl6eq 1520	. . 3 |- (A e. NN -> (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1))) = ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1))))
27	4	seq1lem1 6254	. . . . . . 7 |- (A e. NN -> (1st` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}, <.1, (F` 1)>.) o. `'G)` A)) = A)
28		rdgeq1 3925	. . . . . . . . . . 11 |- (H = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.} -> rec(H, <.1, (F` 1)>.) = rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}, <.1, (F` 1)>.))
29	7, 28	ax-mp 7	. . . . . . . . . 10 |- rec(H, <.1, (F` 1)>.) = rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}, <.1, (F` 1)>.)
30	29	coeq1i 3278	. . . . . . . . 9 |- (rec(H, <.1, (F` 1)>.) o. `'G) = (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}, <.1, (F` 1)>.) o. `'G)
31	30	fveq1i 3716	. . . . . . . 8 |- ((rec(H, <.1, (