Theorem frec2uzrdg 10771

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 10761 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 5670	. . . . 5 |- ( z = B -> ( R ` z ) = ( R ` B ) )
3		fveq2 5670	. . . . . 6 |- ( z = B -> ( G ` z ) = ( G ` B ) )
4	2	fveq2d 5674	. . . . . 6 |- ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
5	3, 4	opeq12d 3891	. . . . 5 |- ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
6	2, 5	eqeq12d 2247	. . . 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 5670	. . . . 5 |- ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
9		fveq2 5670	. . . . . 6 |- ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
10	8	fveq2d 5674	. . . . . 6 |- ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
11	9, 10	opeq12d 3891	. . . . 5 |- ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
12	8, 11	eqeq12d 2247	. . . 4 |- ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
13		fveq2 5670	. . . . 5 |- ( z = v -> ( R ` z ) = ( R ` v ) )
14		fveq2 5670	. . . . . 6 |- ( z = v -> ( G ` z ) = ( G ` v ) )
15	13	fveq2d 5674	. . . . . 6 |- ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
16	14, 15	opeq12d 3891	. . . . 5 |- ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
17	13, 16	eqeq12d 2247	. . . 4 |- ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
18		fveq2 5670	. . . . 5 |- ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
19		fveq2 5670	. . . . . 6 |- ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
20	18	fveq2d 5674	. . . . . 6 |- ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
21	19, 20	opeq12d 3891	. . . . 5 |- ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
22	18, 21	eqeq12d 2247	. . . 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 5671	. . . . . 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 4344	. . . . . . . 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 6628	. . . . . . 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 2277	. . . . 5 |- ( ph -> ( R ` (/) ) = <. C , A >. )
32		frec2uz.2	. . . . . . 7 |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
33	25, 32	frec2uz0d 10761	. . . . . 6 |- ( ph -> ( G ` (/) ) = C )
34	31	fveq2d 5674	. . . . . . 7 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. ) )
35		uzid 9868	. . . . . . . . 9 |- ( C e. ZZ -> C e. ( ZZ>= ` C ) )
36	25, 35	syl 14	. . . . . . . 8 |- ( ph -> C e. ( ZZ>= ` C ) )
37		op2ndg 6345	. . . . . . . 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 2265	. . . . . 6 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = A )
40	33, 39	opeq12d 3891	. . . . 5 |- ( ph -> <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >. )
41	31, 40	eqtr4d 2268	. . . 4 |- ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
42		1st2nd2 6369	. . . . . . . . . . . . . . 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 5674	. . . . . . . . . . . . 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 6053	. . . . . . . . . . . . . . 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 6359	. . . . . . . . . . . . . . . . 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 6360	. . . . . . . . . . . . . . . . 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 9915	. . . . . . . . . . . . . . . . . 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 2624	. . . . . . . . . . . . . . . . . . 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 6057	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( 1st ` z ) -> ( x F y ) = ( ( 1st ` z ) F y ) )
56	55	eleq1d 2301	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( 1st ` z ) -> ( ( x F y ) e. S <-> ( ( 1st ` z ) F y ) e. S ) )
57		oveq2 6058	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( 2nd ` z ) -> ( ( 1st ` z ) F y ) = ( ( 1st ` z ) F ( 2nd ` z ) ) )
58	57	eleq1d 2301	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( 2nd ` z ) -> ( ( ( 1st ` z ) F y ) e. S <-> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
59	56, 58	rspc2v 2934	. . . . . . . . . . . . . . . . . . 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 4779	. . . . . . . . . . . . . . . . 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 6057	. . . . . . . . . . . . . . . . . 18 |- ( x = ( 1st ` z ) -> ( x + 1 ) = ( ( 1st ` z ) + 1 ) )
65	64, 55	opeq12d 3891	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` z ) -> <. ( x + 1 ) , ( x F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. )
66	57	opeq2d 3890	. . . . . . . . . . . . . . . . 17 |- ( y = ( 2nd ` z ) -> <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
67		eqid 2232	. . . . . . . . . . . . . . . . 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 6188	. . . . . . . . . . . . . . . 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 1274	. . . . . . . . . . . . . . 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 2279	. . . . . . . . . . . . . 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 2309	. . . . . . . . . . . . 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 2309	. . . . . . . . . . . 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 2615	. . . . . . . . . . 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 4779	. . . . . . . . . . . 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 6638	. . . . . . . . . . 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 1274	. . . . . . . . . 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 5671	. . . . . . . . . 10 |- ( R ` suc v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v )
82	23	fveq1i 5671	. . . . . . . . . . 11 |- ( R ` v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v )
83	82	fveq2i 5673	. . . . . . . . . 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 2290	. . . . . . . . 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 5670	. . . . . . . . 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 6053	. . . . . . . . . 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 10764	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ( ZZ>= ` C ) )
90	25, 32, 26, 52, 23	frecuzrdgrrn 10770	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( R ` v ) e. ( ( ZZ>= ` C ) X. S ) )
91		xp2nd 6360	. . . . . . . . . . . 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 9915	. . . . . . . . . . . . 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 6207	. . . . . . . . . . . . . 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 6208	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
98		opelxp 4779	. . . . . . . . . . . 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 6057	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w + 1 ) = ( ( G ` v ) + 1 ) )
101		oveq1 6057	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
102	100, 101	opeq12d 3891	. . . . . . . . . . . 12 |- ( w = ( G ` v ) -> <. ( w + 1 ) , ( w F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. )
103		oveq2 6058	. . . . . . . . . . . . 13 |- ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
104	103	opeq2d 3890	. . . . . . . . . . . 12 |- ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
105		oveq1 6057	. . . . . . . . . . . . . 14 |- ( x = w -> ( x + 1 ) = ( w + 1 ) )
106		oveq1 6057	. . . . . . . . . . . . . 14 |- ( x = w -> ( x F y ) = ( w F y ) )
107	105, 106	opeq12d 3891	. . . . . . . . . . . . 13 |- ( x = w -> <. ( x + 1 ) , ( x F y ) >. = <. ( w + 1 ) , ( w F y ) >. )
108		oveq2 6058	. . . . . . . . . . . . . 14 |- ( y = z -> ( w F y ) = ( w F z ) )
109	108	opeq2d 3890	. . . . . . . . . . . . 13 |- ( y = z -> <. ( w + 1 ) , ( w F y ) >. = <. ( w + 1 ) , ( w F z ) >. )
110	107, 109	cbvmpov 6133	. . . . . . . . . . . 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 6188	. . . . . . . . . . 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 1274	. . . . . . . . . 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 2279	. . . . . . . . 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 2287	. . . . . . . 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 2265	. . . . . . 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 10763	. . . . . . . . 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 5674	. . . . . . . . 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 10762	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ZZ )
120	119	peano2zd 9703	. . . . . . . . . . 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 6345	. . . . . . . . . 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 2265	. . . . . . . 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 3891	. . . . . . 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 2268	. . . . . 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 4723	. . 3 |- ( z e. om -> ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) )
131	7, 130	vtoclga 2881	. 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 1398   e. wcel 2203   A.wral 2520   _Vcvv 2813   (/)c0 3508   <.cop 3692   |-> cmpt 4171   suc csuc 4486   omcom 4712   X. cxp 4747   ` cfv 5352  (class class class)co 6050   e. cmpo 6052   1stc1st 6332   2ndc2nd 6333  freccfrec 6621   1c1 8128   + caddc 8130   ZZcz 9577   ZZ>=cuz 9853

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-iinf 4710  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-id 4414  df-iord 4487  df-on 4489  df-ilim 4490  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-1st 6334  df-2nd 6335  df-recs 6536  df-frec 6622  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-n0 9497  df-z 9578  df-uz 9854

This theorem is referenced by:  frecuzrdglem  10773  frecuzrdgtcl  10774  frecuzrdgsuc  10776