Theorem seqval 4665

Description: Value of the infinite sequence builder operation.

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

Distinct variable group(s):   x,y,G   x,H,y   x,z,w,F,y   x,S,y,z,w

Proof of Theorem seqval

Step	Hyp	Ref	Expression
1		seqval.1	. 2 |- S e. V
2		seqval.2	. 2 |- F e. V
3		nnex 4431	. . . 4 |- NN e. V
4		moeq 1431	. . . . 5 |- E*y y = (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` x))
5	4	a1i 7	. . . 4 |- (x e. NN -> E*y y = (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` x)))
6	3, 5	funopabex 2742	. . 3 |- {<.x, y>. | (x e. NN /\ y = (2nd` ((rec(H, <.1, (F` 1)>.) o. `'G)` x)))} e. V
7		opreq 3005	. . . . . . . . . . . . . 14 |- (f = S -> ((2nd` z)f(g` ((1st` z) + 1))) = ((2nd` z)S(g` ((1st` z) + 1))))
8		opeq2 1877	. . . . . . . . . . . . . 14 |- (((2nd` z)f(g` ((1st` z) + 1))) = ((2nd` z)S(g` ((1st` z) + 1))) -> <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.)
9	7, 8	syl 12	. . . . . . . . . . . . 13 |- (f = S -> <.((1st` z) + 1), ((2nd` z)f(g` ((1st` z) + 1)))>. = <.((1st` z) + 1), ((2nd` z)S(g` ((1st` z) + 1)))>.)
10	9	cleq2d 1112	. . . . . . . . . . . 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)))>.))
11	10	biopabdv 2102	. . . . . . . . . . 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)))>.})
12		rdgeq1 2972	. . . . . . . . . . 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)>.))
13	11, 12	syl 12	. . . . . . . . . 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)>.))
14	13	coeq1d 2506	. . . . . . . . 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)))
15		seqval.3	. . . . . . . . . . 11 |- G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om)
16		cnveq 2513	. . . . . . . . . . 11 |- (G = (rec({<.z, w>. | w = (z + 1)}, 1) |` om) -> `'G = `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om))
17	15, 16	ax-mp 6	. . . . . . . . . 10 |- `'G = `'(rec({<.z, w>. | w = (z + 1)}, 1) |` om)
18	17	coeq2i 2505	. . . . . . . . 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))
19	14, 18	syl6eqr 1142	. . . . . . . 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))
20	19	fveq1d 2834	. . . . . . 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))
21	20	fveq2d 2836	. . . . . 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)))
22	21	cleq2d 1112	. . . . 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))))
23	22	anbi2d 468	. . . 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