Theorem seqsuclem 4669

Description: Lemma for seqsuc 4671.

Hypotheses

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

Assertion

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

Distinct variable group(s):   z,w,F   z,S,w

Proof of Theorem seqsuclem

Step	Hyp	Ref	Expression
1		nnz 4582	. . . . . . . 8 |- NN = {x e. ZZ | 1 <_ x}
2	1	eleq2i 1153	. . . . . . 7 |- (A e. NN <-> A e. {x e. ZZ | 1 <_ x})
3		1z 4584	. . . . . . . 8 |- 1 e. ZZ
4		seqval.3	. . . . . . . 8 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
5	3, 4	uzrdgsuc 4659	. . . . . . 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 174	. . . . . 6 |- (A e. NN -> ((rec(H, <.1, (F` 1)>.) o. `'G)` (A + 1)) = (H` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)))
7		seqval.4	. . . . . . . 8 |- H = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}
8		opeq12 1878	. . . . . . . . . . . 12 |- ((((1st` x) + 1) = ((1st` z) + 1) /\ ((2nd` x)S(F` ((1st` x) + 1))) = ((2nd` z)S(F` ((1st` z) + 1)))) -> <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.)
9		fveq2 2832	. . . . . . . . . . . . 13 |- (x = z -> (1st` x) = (1st` z))
10	9	opreq1d 3012	. . . . . . . . . . . 12 |- (x = z -> ((1st` x) + 1) = ((1st` z) + 1))
11		fveq2 2832	. . . . . . . . . . . . 13 |- (x = z -> (2nd` x) = (2nd` z))
12	10	fveq2d 2836	. . . . . . . . . . . . 13 |- (x = z -> (F` ((1st` x) + 1)) = (F` ((1st` z) + 1)))
13	11, 12	opreq12d 3014	. . . . . . . . . . . 12 |- (x = z -> ((2nd` x)S(F` ((1st` x) + 1))) = ((2nd` z)S(F` ((1st` z) + 1))))
14	8, 10, 13	sylanc 361	. . . . . . . . . . 11 |- (x = z -> <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.)
15	14	cleq2d 1112	. . . . . . . . . 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)))>.))
16		cleq1 1107	. . . . . . . . . 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)))>.))
17	15, 16	sylan9bb 418	. . . . . . . . 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)))>.))
18	17	cbvopabv 2105	. . . . . . . 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)))>.}
19	7, 18	eqtr4 1122	. . . . . . 7 |- H = {<.x, y>. | y = <.((1st` x) + 1), ((2nd` x)S(F` ((1st` x) + 1)))>.}
20		fvex 2838	. . . . . . 7 |- ((rec(H, <.1, (F` 1)>.) o. `'G)` A) e. V
21	19, 20	seqrval 4664	. . . . . 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)))>.
22	6, 21	syl6eq 1140	. . . . 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)))>.)
23	22	fveq2d 2836	. . . 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)))>.))
24		oprex 3018	. . . . 5 |- ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1) e. V
25		oprex 3018	. . . . 5 |- ((2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` A))S(F` ((1st` ((rec(H, <.1, (F` 1)>.) o. `'G)` A)) + 1))) e. V
26	24, 25	op2nd 3092	. . . 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)))
27	23, 26	syl6eq 1140	. . 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))))
28	4	seqlem1 4662	. . . . . . 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)
29		rdgeq1 2972	. . . . . . . . . . 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)>.))
30	7, 29	ax-mp 6	. . . . . . . . . 10 |- rec(H, <.1, (F` 1)>.) = rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(F` ((1st` z) + 1)))>.}, <.1