Theorem seq1val 6312

Description: Value of the recursive sequence builder operation.

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
seq1val	|- (S seq1 F) = {<.x, y>. | (x e. NN /\ y = (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` x)))}

Distinct variable groups:   x,y,G   x,H,y   x,z,w,F,y   x,S,y,z,w

Proof of Theorem seq1val

Step	Hyp	Ref	Expression
1		seq1val.1	. 2 |- S e. V
2		seq1val.2	. 2 |- F e. V
3		nnex 5933	. . . 4 |- NN e. V
4	3	opabex2 3610	. . 3 |- {<.x, y>. | (x e. NN /\ y = (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` x)))} e. V
5		opreq 3967	. . . . . . . . . . . . . 14 |- (f = S -> ((2nd` z)f(g` ((1st` z) + 1))) = ((2nd` z)S(g` ((1st` z) + 1))))
6	5	opeq2d 2494	. . . . . . . . . . . . 13 |- (f = S -> <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.)
7	6	eqeq2d 1486	. . . . . . . . . . . 12 |- (f = S -> (w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>. <-> w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.))
8	7	opabbidv 2670	. . . . . . . . . . 11 |- (f = S -> {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.} = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.})
9		rdgeq1 3934	. . . . . . . . . . 11 |- ({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.} = {<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.} -> rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) = rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.))
10	8, 9	syl 10	. . . . . . . . . 10 |- (f = S -> rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) = rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.))
11	10	coeq1d 3285	. . . . . . . . 9 |- (f = S -> (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om)) = (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om)))
12		seq1val.3	. . . . . . . . . . 11 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
13		cnveq 3292	. . . . . . . . . . 11 |- (G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om) -> `'G = `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))
14	12, 13	ax-mp 7	. . . . . . . . . 10 |- `'G = `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om)
15	14	coeq2i 3284	. . . . . . . . 9 |- (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G) = (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))
16	11, 15	syl6eqr 1525	. . . . . . . 8 |- (f = S -> (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om)) = (rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G))
17	16	fveq1d 3726	. . . . . . 7 |- (f = S -> ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))` x) = ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G)` x))
18	17	fveq2d 3728	. . . . . 6 |- (f = S -> (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))` x)) = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G)` x)))
19	18	eqeq2d 1486	. . . . 5 |- (f = S -> (y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))` x)) <-> y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G)` x))))
20	19	anbi2d 616	. . . 4 |- (f = S -> ((x e. NN /\ y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))` x))) <-> (x e. NN /\ y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.}, <.1, (g` 1)>.) o. `'G)` x)))))
21	20	opabbidv 2670	. . 3 |- (f = S -> {<.x, y>. | (x e. NN /\ y = (2nd` ((rec({<.z, w>. | w = <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>.},