Theorem frec2uzrdg 10409

Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0) with characteristic function F ( x , y ) and initial value A. This lemma shows that evaluating R at an element of om gives an ordered pair whose first element is the index (translated from om to ( ZZ>= ` C )). See comment in frec2uz0d 10399 which describes G and the index translation. (Contributed by Jim Kingdon, 24-May-2020.)

Hypotheses

Ref	Expression
frec2uz.1	|- ( ph -> C e. ZZ )
frec2uz.2	|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
frecuzrdgrrn.a	|- ( ph -> A e. S )
frecuzrdgrrn.f	|- ( ( ph /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )
frecuzrdgrrn.2	|- R = frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. )
frec2uzrdg.b	|- ( ph -> B e. om )

Assertion

Ref	Expression
frec2uzrdg	|- ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )

Distinct variable groups:   y, A   x, C, y   y, G   x, F, y   x, S, y   ph, x, y

Allowed substitution hints:   A( x)   B( x, y)   R( x, y)   G( x)

Proof of Theorem frec2uzrdg

Dummy variables w z v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frec2uzrdg.b	. 2 |- ( ph -> B e. om )
2		fveq2 5516	. . . . 5 |- ( z = B -> ( R ` z ) = ( R ` B ) )
3		fveq2 5516	. . . . . 6 |- ( z = B -> ( G ` z ) = ( G ` B ) )
4	2	fveq2d 5520	. . . . . 6 |- ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
5	3, 4	opeq12d 3787	. . . . 5 |- ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
6	2, 5	eqeq12d 2192	. . . 4 |- ( z = B -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
7	6	imbi2d 230	. . 3 |- ( z = B -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) ) )
8		fveq2 5516	. . . . 5 |- ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
9		fveq2 5516	. . . . . 6 |- ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
10	8	fveq2d 5520	. . . . . 6 |- ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
11	9, 10	opeq12d 3787	. . . . 5 |- ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
12	8, 11	eqeq12d 2192	. . . 4 |- ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
13		fveq2 5516	. . . . 5 |- ( z = v -> ( R ` z ) = ( R ` v ) )
14		fveq2 5516	. . . . . 6 |- ( z = v -> ( G ` z ) = ( G ` v ) )
15	13	fveq2d 5520	. . . . . 6 |- ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
16	14, 15	opeq12d 3787	. . . . 5 |- ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
17	13, 16	eqeq12d 2192	. . . 4 |- ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
18		fveq2 5516	. . . . 5 |- ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
19		fveq2 5516	. . . . . 6 |- ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
20	18	fveq2d 5520	. . . . . 6 |- ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
21	19, 20	opeq12d 3787	. . . . 5 |- ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
22	18, 21	eqeq12d 2192	. . . 4 |- ( z = suc v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) )
23		frecuzrdgrrn.2	. . . . . . 7 |- R = frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. )
24	23	fveq1i 5517	. . . . . 6 |- ( R ` (/) ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` (/) )
25		frec2uz.1	. . . . . . . 8 |- ( ph -> C e. ZZ )
26		frecuzrdgrrn.a	. . . . . . . 8 |- ( ph -> A e. S )
27		opexg 4229	. . . . . . . 8 |- ( ( C e. ZZ /\ A e. S ) -> <. C , A >. e. _V )
28	25, 26, 27	syl2anc 411	. . . . . . 7 |- ( ph -> <. C , A >. e. _V )
29		frec0g 6398	. . . . . . 7 |- ( <. C , A >. e. _V -> (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` (/) ) = <. C , A >. )
30	28, 29	syl 14	. . . . . 6 |- ( ph -> (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` (/) ) = <. C , A >. )
31	24, 30	eqtrid 2222	. . . . 5 |- ( ph -> ( R ` (/) ) = <. C , A >. )
32		frec2uz.2	. . . . . . 7 |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
33	25, 32	frec2uz0d 10399	. . . . . 6 |- ( ph -> ( G ` (/) ) = C )
34	31	fveq2d 5520	. . . . . . 7 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. ) )
35		uzid 9542	. . . . . . . . 9 |- ( C e. ZZ -> C e. ( ZZ>= ` C ) )
36	25, 35	syl 14	. . . . . . . 8 |- ( ph -> C e. ( ZZ>= ` C ) )
37		op2ndg 6152	. . . . . . . 8 |- ( ( C e. ( ZZ>= ` C ) /\ A e. S ) -> ( 2nd ` <. C , A >. ) = A )
38	36, 26, 37	syl2anc 411	. . . . . . 7 |- ( ph -> ( 2nd ` <. C , A >. ) = A )
39	34, 38	eqtrd 2210	. . . . . 6 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = A )
40	33, 39	opeq12d 3787	. . . . 5 |- ( ph -> <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >. )
41	31, 40	eqtr4d 2213	. . . 4 |- ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
42		1st2nd2 6176	. . . . . . . . . . . . . . 15 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
43	42	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
44	43	fveq2d 5520	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` z ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
45		df-ov 5878	. . . . . . . . . . . . . . 15 |- ( ( 1st ` z ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` z ) ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
46		xp1st 6166	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> ( 1st ` z ) e. ( ZZ>= ` C ) )
47	46	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( 1st ` z ) e. ( ZZ>= ` C ) )
48		xp2nd 6167	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> ( 2nd ` z ) e. S )
49	48	adantl 277	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( 2nd ` z ) e. S )
50		peano2uz 9583	. . . . . . . . . . . . . . . . . 18 |- ( ( 1st ` z ) e. ( ZZ>= ` C ) -> ( ( 1st ` z ) + 1 ) e. ( ZZ>= ` C ) )
51	47, 50	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( 1st ` z ) + 1 ) e. ( ZZ>= ` C ) )
52		frecuzrdgrrn.f	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )
53	52	ralrimivva 2559	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. x e. ( ZZ>= ` C ) A. y e. S ( x F y ) e. S )
54	53	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> A. x e. ( ZZ>= ` C ) A. y e. S ( x F y ) e. S )
55		oveq1 5882	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( 1st ` z ) -> ( x F y ) = ( ( 1st ` z ) F y ) )
56	55	eleq1d 2246	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( 1st ` z ) -> ( ( x F y ) e. S <-> ( ( 1st ` z ) F y ) e. S ) )
57		oveq2 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( 2nd ` z ) -> ( ( 1st ` z ) F y ) = ( ( 1st ` z ) F ( 2nd ` z ) ) )
58	57	eleq1d 2246	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( 2nd ` z ) -> ( ( ( 1st ` z ) F y ) e. S <-> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
59	56, 58	rspc2v 2855	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1st ` z ) e. ( ZZ>= ` C ) /\ ( 2nd ` z ) e. S ) -> ( A. x e. ( ZZ>= ` C ) A. y e. S ( x F y ) e. S -> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
60	47, 49, 59	syl2anc 411	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( A. x e. ( ZZ>= ` C ) A. y e. S ( x F y ) e. S -> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
61	54, 60	mpd 13	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S )
62		opelxp 4657	. . . . . . . . . . . . . . . . 17 |- ( <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. e. ( ( ZZ>= ` C ) X. S ) <-> ( ( ( 1st ` z ) + 1 ) e. ( ZZ>= ` C ) /\ ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
63	51, 61, 62	sylanbrc 417	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. e. ( ( ZZ>= ` C ) X. S ) )
64		oveq1 5882	. . . . . . . . . . . . . . . . . 18 |- ( x = ( 1st ` z ) -> ( x + 1 ) = ( ( 1st ` z ) + 1 ) )
65	64, 55	opeq12d 3787	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` z ) -> <. ( x + 1 ) , ( x F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. )
66	57	opeq2d 3786	. . . . . . . . . . . . . . . . 17 |- ( y = ( 2nd ` z ) -> <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
67		eqid 2177	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) = ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. )
68	65, 66, 67	ovmpog 6009	. . . . . . . . . . . . . . . 16 |- ( ( ( 1st ` z ) e. ( ZZ>= ` C ) /\ ( 2nd ` z ) e. S /\ <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( 1st ` z ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` z ) ) = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
69	47, 49, 63, 68	syl3anc 1238	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( 1st ` z ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` z ) ) = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
70	45, 69	eqtr3id 2224	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
71	70, 63	eqeltrd 2254	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) e. ( ( ZZ>= ` C ) X. S ) )
72	44, 71	eqeltrd 2254	. . . . . . . . . . . 12 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` z ) e. ( ( ZZ>= ` C ) X. S ) )
73	72	ralrimiva 2550	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> A. z e. ( ( ZZ>= ` C ) X. S ) ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` z ) e. ( ( ZZ>= ` C ) X. S ) )
74	36	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> C e. ( ZZ>= ` C ) )
75	26	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> A e. S )
76		opelxp 4657	. . . . . . . . . . . 12 |- ( <. C , A >. e. ( ( ZZ>= ` C ) X. S ) <-> ( C e. ( ZZ>= ` C ) /\ A e. S ) )
77	74, 75, 76	sylanbrc 417	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> <. C , A >. e. ( ( ZZ>= ` C ) X. S ) )
78		simpr 110	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> v e. om )
79		frecsuc 6408	. . . . . . . . . . 11 |- ( ( A. z e. ( ( ZZ>= ` C ) X. S ) ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` z ) e. ( ( ZZ>= ` C ) X. S ) /\ <. C , A >. e. ( ( ZZ>= ` C ) X. S ) /\ v e. om ) -> (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v ) ) )
80	73, 77, 78, 79	syl3anc 1238	. . . . . . . . . 10 |- ( ( ph /\ v e. om ) -> (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v ) ) )
81	23	fveq1i 5517	. . . . . . . . . 10 |- ( R ` suc v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v )
82	23	fveq1i 5517	. . . . . . . . . . 11 |- ( R ` v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v )
83	82	fveq2i 5519	. . . . . . . . . 10 |- ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v ) )
84	80, 81, 83	3eqtr4g 2235	. . . . . . . . 9 |- ( ( ph /\ v e. om ) -> ( R ` suc v ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) )
85	84	adantr 276	. . . . . . . 8 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( R ` suc v ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) )
86		fveq2 5516	. . . . . . . . 9 |- ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
87		df-ov 5878	. . . . . . . . . 10 |- ( ( G ` v ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
88	25	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> C e. ZZ )
89	88, 32, 78	frec2uzuzd 10402	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ( ZZ>= ` C ) )
90	25, 32, 26, 52, 23	frecuzrdgrrn 10408	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( R ` v ) e. ( ( ZZ>= ` C ) X. S ) )
91		xp2nd 6167	. . . . . . . . . . . 12 |- ( ( R ` v ) e. ( ( ZZ>= ` C ) X. S ) -> ( 2nd ` ( R ` v ) ) e. S )
92	90, 91	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( 2nd ` ( R ` v ) ) e. S )
93		peano2uz 9583	. . . . . . . . . . . . 13 |- ( ( G ` v ) e. ( ZZ>= ` C ) -> ( ( G ` v ) + 1 ) e. ( ZZ>= ` C ) )
94	89, 93	syl 14	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) + 1 ) e. ( ZZ>= ` C ) )
95	52	caovclg 6027	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z e. ( ZZ>= ` C ) /\ w e. S ) ) -> ( z F w ) e. S )
96	95	adantlr 477	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. om ) /\ ( z e. ( ZZ>= ` C ) /\ w e. S ) ) -> ( z F w ) e. S )
97	96, 89, 92	caovcld 6028	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
98		opelxp 4657	. . . . . . . . . . . 12 |- ( <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. ( ( ZZ>= ` C ) X. S ) <-> ( ( ( G ` v ) + 1 ) e. ( ZZ>= ` C ) /\ ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S ) )
99	94, 97, 98	sylanbrc 417	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. ( ( ZZ>= ` C ) X. S ) )
100		oveq1 5882	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w + 1 ) = ( ( G ` v ) + 1 ) )
101		oveq1 5882	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
102	100, 101	opeq12d 3787	. . . . . . . . . . . 12 |- ( w = ( G ` v ) -> <. ( w + 1 ) , ( w F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. )
103		oveq2 5883	. . . . . . . . . . . . 13 |- ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
104	103	opeq2d 3786	. . . . . . . . . . . 12 |- ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
105		oveq1 5882	. . . . . . . . . . . . . 14 |- ( x = w -> ( x + 1 ) = ( w + 1 ) )
106		oveq1 5882	. . . . . . . . . . . . . 14 |- ( x = w -> ( x F y ) = ( w F y ) )
107	105, 106	opeq12d 3787	. . . . . . . . . . . . 13 |- ( x = w -> <. ( x + 1 ) , ( x F y ) >. = <. ( w + 1 ) , ( w F y ) >. )
108		oveq2 5883	. . . . . . . . . . . . . 14 |- ( y = z -> ( w F y ) = ( w F z ) )
109	108	opeq2d 3786	. . . . . . . . . . . . 13 |- ( y = z -> <. ( w + 1 ) , ( w F y ) >. = <. ( w + 1 ) , ( w F z ) >. )
110	107, 109	cbvmpov 5955	. . . . . . . . . . . 12 |- ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) = ( w e. ( ZZ>= ` C ) , z e. S |-> <. ( w + 1 ) , ( w F z ) >. )
111	102, 104, 110	ovmpog 6009	. . . . . . . . . . 11 |- ( ( ( G ` v ) e. ( ZZ>= ` C ) /\ ( 2nd ` ( R ` v ) ) e. S /\ <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. ( ( ZZ>= ` C ) X. S ) ) -> ( ( G ` v ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
112	89, 92, 99, 111	syl3anc 1238	. . . . . . . . . 10 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` v ) ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
113	87, 112	eqtr3id 2224	. . . . . . . . 9 |- ( ( ph /\ v e. om ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
114	86, 113	sylan9eqr 2232	. . . . . . . 8 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` v ) ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
115	85, 114	eqtrd 2210	. . . . . . 7 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( R ` suc v ) = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
116	88, 32, 78	frec2uzsucd 10401	. . . . . . . . 9 |- ( ( ph /\ v e. om ) -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
117	116	adantr 276	. . . . . . . 8 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
118	115	fveq2d 5520	. . . . . . . . 9 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( 2nd ` ( R ` suc v ) ) = ( 2nd ` <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) )
119	88, 32, 78	frec2uzzd 10400	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ZZ )
120	119	peano2zd 9378	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) + 1 ) e. ZZ )
121	120	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ( G ` v ) + 1 ) e. ZZ )
122	97	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
123		op2ndg 6152	. . . . . . . . . 10 |- ( ( ( ( G ` v ) + 1 ) e. ZZ /\ ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S ) -> ( 2nd ` <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
124	121, 122, 123	syl2anc 411	. . . . . . . . 9 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( 2nd ` <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
125	118, 124	eqtrd 2210	. . . . . . . 8 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( 2nd ` ( R ` suc v ) ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
126	117, 125	opeq12d 3787	. . . . . . 7 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
127	115, 126	eqtr4d 2213	. . . . . 6 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
128	127	ex 115	. . . . 5 |- ( ( ph /\ v e. om ) -> ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) )
129	128	expcom 116	. . . 4 |- ( v e. om -> ( ph -> ( ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. -> ( R ` suc v ) = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. ) ) )
130	12, 17, 22, 41, 129	finds2 4601	. . 3 |- ( z e. om -> ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) )
131	7, 130	vtoclga 2804	. 2 |- ( B e. om -> ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
132	1, 131	mpcom 36	1 |- ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148   A.wral 2455   _Vcvv 2738   (/)c0 3423   <.cop 3596   |-> cmpt 4065   suc csuc 4366   omcom 4590   X. cxp 4625   ` cfv 5217  (class class class)co 5875   e. cmpo 5877   1stc1st 6139   2ndc2nd 6140  freccfrec 6391   1c1 7812   + caddc 7814   ZZcz 9253   ZZ>=cuz 9528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-addcom 7911  ax-addass 7913  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-0id 7919  ax-rnegex 7920  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-ltadd 7927

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-inn 8920  df-n0 9177  df-z 9254  df-uz 9529

This theorem is referenced by:  frecuzrdglem  10411  frecuzrdgtcl  10412  frecuzrdgsuc  10414