Theorem frec2uzrdg 10069

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 10059 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 5373	. . . . 5 |- ( z = B -> ( R ` z ) = ( R ` B ) )
3		fveq2 5373	. . . . . 6 |- ( z = B -> ( G ` z ) = ( G ` B ) )
4	2	fveq2d 5377	. . . . . 6 |- ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
5	3, 4	opeq12d 3677	. . . . 5 |- ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
6	2, 5	eqeq12d 2127	. . . 4 |- ( z = B -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) )
7	6	imbi2d 229	. . 3 |- ( z = B -> ( ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) <-> ( ph -> ( R ` B ) = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. ) ) )
8		fveq2 5373	. . . . 5 |- ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
9		fveq2 5373	. . . . . 6 |- ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
10	8	fveq2d 5377	. . . . . 6 |- ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
11	9, 10	opeq12d 3677	. . . . 5 |- ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
12	8, 11	eqeq12d 2127	. . . 4 |- ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
13		fveq2 5373	. . . . 5 |- ( z = v -> ( R ` z ) = ( R ` v ) )
14		fveq2 5373	. . . . . 6 |- ( z = v -> ( G ` z ) = ( G ` v ) )
15	13	fveq2d 5377	. . . . . 6 |- ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
16	14, 15	opeq12d 3677	. . . . 5 |- ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
17	13, 16	eqeq12d 2127	. . . 4 |- ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
18		fveq2 5373	. . . . 5 |- ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
19		fveq2 5373	. . . . . 6 |- ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
20	18	fveq2d 5377	. . . . . 6 |- ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
21	19, 20	opeq12d 3677	. . . . 5 |- ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
22	18, 21	eqeq12d 2127	. . . 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 5374	. . . . . 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 4108	. . . . . . . 8 |- ( ( C e. ZZ /\ A e. S ) -> <. C , A >. e. _V )
28	25, 26, 27	syl2anc 406	. . . . . . 7 |- ( ph -> <. C , A >. e. _V )
29		frec0g 6246	. . . . . . 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	syl5eq 2157	. . . . 5 |- ( ph -> ( R ` (/) ) = <. C , A >. )
32		frec2uz.2	. . . . . . 7 |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
33	25, 32	frec2uz0d 10059	. . . . . 6 |- ( ph -> ( G ` (/) ) = C )
34	31	fveq2d 5377	. . . . . . 7 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. ) )
35		uzid 9236	. . . . . . . . 9 |- ( C e. ZZ -> C e. ( ZZ>= ` C ) )
36	25, 35	syl 14	. . . . . . . 8 |- ( ph -> C e. ( ZZ>= ` C ) )
37		op2ndg 6001	. . . . . . . 8 |- ( ( C e. ( ZZ>= ` C ) /\ A e. S ) -> ( 2nd ` <. C , A >. ) = A )
38	36, 26, 37	syl2anc 406	. . . . . . 7 |- ( ph -> ( 2nd ` <. C , A >. ) = A )
39	34, 38	eqtrd 2145	. . . . . 6 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = A )
40	33, 39	opeq12d 3677	. . . . 5 |- ( ph -> <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >. )
41	31, 40	eqtr4d 2148	. . . 4 |- ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
42		1st2nd2 6025	. . . . . . . . . . . . . . 15 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
43	42	adantl 273	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
44	43	fveq2d 5377	. . . . . . . . . . . . 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 5729	. . . . . . . . . . . . . . 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 6015	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> ( 1st ` z ) e. ( ZZ>= ` C ) )
47	46	adantl 273	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( 1st ` z ) e. ( ZZ>= ` C ) )
48		xp2nd 6016	. . . . . . . . . . . . . . . . 17 |- ( z e. ( ( ZZ>= ` C ) X. S ) -> ( 2nd ` z ) e. S )
49	48	adantl 273	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ v e. om ) /\ z e. ( ( ZZ>= ` C ) X. S ) ) -> ( 2nd ` z ) e. S )
50		peano2uz 9274	. . . . . . . . . . . . . . . . . 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 2486	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. x e. ( ZZ>= ` C ) A. y e. S ( x F y ) e. S )
54	53	ad2antrr 477	. . . . . . . . . . . . . . . . . 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 5733	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( 1st ` z ) -> ( x F y ) = ( ( 1st ` z ) F y ) )
56	55	eleq1d 2181	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( 1st ` z ) -> ( ( x F y ) e. S <-> ( ( 1st ` z ) F y ) e. S ) )
57		oveq2 5734	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( 2nd ` z ) -> ( ( 1st ` z ) F y ) = ( ( 1st ` z ) F ( 2nd ` z ) ) )
58	57	eleq1d 2181	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( 2nd ` z ) -> ( ( ( 1st ` z ) F y ) e. S <-> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
59	56, 58	rspc2v 2770	. . . . . . . . . . . . . . . . . . 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 406	. . . . . . . . . . . . . . . . . 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 4527	. . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . 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 5733	. . . . . . . . . . . . . . . . . 18 |- ( x = ( 1st ` z ) -> ( x + 1 ) = ( ( 1st ` z ) + 1 ) )
65	64, 55	opeq12d 3677	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` z ) -> <. ( x + 1 ) , ( x F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. )
66	57	opeq2d 3676	. . . . . . . . . . . . . . . . 17 |- ( y = ( 2nd ` z ) -> <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
67		eqid 2113	. . . . . . . . . . . . . . . . 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 5857	. . . . . . . . . . . . . . . 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 1197	. . . . . . . . . . . . . . 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	syl5eqr 2159	. . . . . . . . . . . . . 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 2189	. . . . . . . . . . . . 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 2189	. . . . . . . . . . . 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 2477	. . . . . . . . . . 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 272	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> C e. ( ZZ>= ` C ) )
75	26	adantr 272	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> A e. S )
76		opelxp 4527	. . . . . . . . . . . 12 |- ( <. C , A >. e. ( ( ZZ>= ` C ) X. S ) <-> ( C e. ( ZZ>= ` C ) /\ A e. S ) )
77	74, 75, 76	sylanbrc 411	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> <. C , A >. e. ( ( ZZ>= ` C ) X. S ) )
78		simpr 109	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> v e. om )
79		frecsuc 6256	. . . . . . . . . . 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 1197	. . . . . . . . . 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 5374	. . . . . . . . . 10 |- ( R ` suc v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v )
82	23	fveq1i 5374	. . . . . . . . . . 11 |- ( R ` v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v )
83	82	fveq2i 5376	. . . . . . . . . 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 2170	. . . . . . . . 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 272	. . . . . . . 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 5373	. . . . . . . . 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 5729	. . . . . . . . . 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 272	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> C e. ZZ )
89	88, 32, 78	frec2uzuzd 10062	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ( ZZ>= ` C ) )
90	25, 32, 26, 52, 23	frecuzrdgrrn 10068	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( R ` v ) e. ( ( ZZ>= ` C ) X. S ) )
91		xp2nd 6016	. . . . . . . . . . . 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 9274	. . . . . . . . . . . . 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 5875	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z e. ( ZZ>= ` C ) /\ w e. S ) ) -> ( z F w ) e. S )
96	95	adantlr 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ v e. om ) /\ ( z e. ( ZZ>= ` C ) /\ w e. S ) ) -> ( z F w ) e. S )
97	96, 89, 92	caovcld 5876	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
98		opelxp 4527	. . . . . . . . . . . 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 411	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. e. ( ( ZZ>= ` C ) X. S ) )
100		oveq1 5733	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w + 1 ) = ( ( G ` v ) + 1 ) )
101		oveq1 5733	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
102	100, 101	opeq12d 3677	. . . . . . . . . . . 12 |- ( w = ( G ` v ) -> <. ( w + 1 ) , ( w F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. )
103		oveq2 5734	. . . . . . . . . . . . 13 |- ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
104	103	opeq2d 3676	. . . . . . . . . . . 12 |- ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
105		oveq1 5733	. . . . . . . . . . . . . 14 |- ( x = w -> ( x + 1 ) = ( w + 1 ) )
106		oveq1 5733	. . . . . . . . . . . . . 14 |- ( x = w -> ( x F y ) = ( w F y ) )
107	105, 106	opeq12d 3677	. . . . . . . . . . . . 13 |- ( x = w -> <. ( x + 1 ) , ( x F y ) >. = <. ( w + 1 ) , ( w F y ) >. )
108		oveq2 5734	. . . . . . . . . . . . . 14 |- ( y = z -> ( w F y ) = ( w F z ) )
109	108	opeq2d 3676	. . . . . . . . . . . . 13 |- ( y = z -> <. ( w + 1 ) , ( w F y ) >. = <. ( w + 1 ) , ( w F z ) >. )
110	107, 109	cbvmpov 5803	. . . . . . . . . . . 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 5857	. . . . . . . . . . 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 1197	. . . . . . . . . 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	syl5eqr 2159	. . . . . . . . 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 2167	. . . . . . . 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 2145	. . . . . . 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 10061	. . . . . . . . 9 |- ( ( ph /\ v e. om ) -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
117	116	adantr 272	. . . . . . . 8 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( G ` suc v ) = ( ( G ` v ) + 1 ) )
118	115	fveq2d 5377	. . . . . . . . 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 10060	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ZZ )
120	119	peano2zd 9074	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) + 1 ) e. ZZ )
121	120	adantr 272	. . . . . . . . . 10 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ( G ` v ) + 1 ) e. ZZ )
122	97	adantr 272	. . . . . . . . . 10 |- ( ( ( ph /\ v e. om ) /\ ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
123		op2ndg 6001	. . . . . . . . . 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 406	. . . . . . . . 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 2145	. . . . . . . 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 3677	. . . . . . 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 2148	. . . . . 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 114	. . . . 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 115	. . . 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 4473	. . 3 |- ( z e. om -> ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) )
131	7, 130	vtoclga 2721	. 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 103   = wceq 1312   e. wcel 1461   A.wral 2388   _Vcvv 2655   (/)c0 3327   <.cop 3494   |-> cmpt 3947   suc csuc 4245   omcom 4462   X. cxp 4495   ` cfv 5079  (class class class)co 5726   e. cmpo 5728   1stc1st 5988   2ndc2nd 5989  freccfrec 6239   1c1 7542   + caddc 7544   ZZcz 8952   ZZ>=cuz 9222

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-ltadd 7655

This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-frec 6240  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-inn 8625  df-n0 8876  df-z 8953  df-uz 9223

This theorem is referenced by:  frecuzrdglem  10071  frecuzrdgtcl  10072  frecuzrdgsuc  10074