Theorem frec2uzrdg 10501

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 10491 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 5558	. . . . 5 |- ( z = B -> ( R ` z ) = ( R ` B ) )
3		fveq2 5558	. . . . . 6 |- ( z = B -> ( G ` z ) = ( G ` B ) )
4	2	fveq2d 5562	. . . . . 6 |- ( z = B -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` B ) ) )
5	3, 4	opeq12d 3816	. . . . 5 |- ( z = B -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` B ) , ( 2nd ` ( R ` B ) ) >. )
6	2, 5	eqeq12d 2211	. . . 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 5558	. . . . 5 |- ( z = (/) -> ( R ` z ) = ( R ` (/) ) )
9		fveq2 5558	. . . . . 6 |- ( z = (/) -> ( G ` z ) = ( G ` (/) ) )
10	8	fveq2d 5562	. . . . . 6 |- ( z = (/) -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` (/) ) ) )
11	9, 10	opeq12d 3816	. . . . 5 |- ( z = (/) -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
12	8, 11	eqeq12d 2211	. . . 4 |- ( z = (/) -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. ) )
13		fveq2 5558	. . . . 5 |- ( z = v -> ( R ` z ) = ( R ` v ) )
14		fveq2 5558	. . . . . 6 |- ( z = v -> ( G ` z ) = ( G ` v ) )
15	13	fveq2d 5562	. . . . . 6 |- ( z = v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` v ) ) )
16	14, 15	opeq12d 3816	. . . . 5 |- ( z = v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. )
17	13, 16	eqeq12d 2211	. . . 4 |- ( z = v -> ( ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. <-> ( R ` v ) = <. ( G ` v ) , ( 2nd ` ( R ` v ) ) >. ) )
18		fveq2 5558	. . . . 5 |- ( z = suc v -> ( R ` z ) = ( R ` suc v ) )
19		fveq2 5558	. . . . . 6 |- ( z = suc v -> ( G ` z ) = ( G ` suc v ) )
20	18	fveq2d 5562	. . . . . 6 |- ( z = suc v -> ( 2nd ` ( R ` z ) ) = ( 2nd ` ( R ` suc v ) ) )
21	19, 20	opeq12d 3816	. . . . 5 |- ( z = suc v -> <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. = <. ( G ` suc v ) , ( 2nd ` ( R ` suc v ) ) >. )
22	18, 21	eqeq12d 2211	. . . 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 5559	. . . . . 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 4261	. . . . . . . 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 6455	. . . . . . 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 2241	. . . . 5 |- ( ph -> ( R ` (/) ) = <. C , A >. )
32		frec2uz.2	. . . . . . 7 |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )
33	25, 32	frec2uz0d 10491	. . . . . 6 |- ( ph -> ( G ` (/) ) = C )
34	31	fveq2d 5562	. . . . . . 7 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = ( 2nd ` <. C , A >. ) )
35		uzid 9615	. . . . . . . . 9 |- ( C e. ZZ -> C e. ( ZZ>= ` C ) )
36	25, 35	syl 14	. . . . . . . 8 |- ( ph -> C e. ( ZZ>= ` C ) )
37		op2ndg 6209	. . . . . . . 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 2229	. . . . . 6 |- ( ph -> ( 2nd ` ( R ` (/) ) ) = A )
40	33, 39	opeq12d 3816	. . . . 5 |- ( ph -> <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. = <. C , A >. )
41	31, 40	eqtr4d 2232	. . . 4 |- ( ph -> ( R ` (/) ) = <. ( G ` (/) ) , ( 2nd ` ( R ` (/) ) ) >. )
42		1st2nd2 6233	. . . . . . . . . . . . . . 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 5562	. . . . . . . . . . . . 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 5925	. . . . . . . . . . . . . . 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 6223	. . . . . . . . . . . . . . . . 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 6224	. . . . . . . . . . . . . . . . 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 9657	. . . . . . . . . . . . . . . . . 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 2579	. . . . . . . . . . . . . . . . . . 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 5929	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( 1st ` z ) -> ( x F y ) = ( ( 1st ` z ) F y ) )
56	55	eleq1d 2265	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( 1st ` z ) -> ( ( x F y ) e. S <-> ( ( 1st ` z ) F y ) e. S ) )
57		oveq2 5930	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( 2nd ` z ) -> ( ( 1st ` z ) F y ) = ( ( 1st ` z ) F ( 2nd ` z ) ) )
58	57	eleq1d 2265	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( 2nd ` z ) -> ( ( ( 1st ` z ) F y ) e. S <-> ( ( 1st ` z ) F ( 2nd ` z ) ) e. S ) )
59	56, 58	rspc2v 2881	. . . . . . . . . . . . . . . . . . 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 4693	. . . . . . . . . . . . . . . . 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 5929	. . . . . . . . . . . . . . . . . 18 |- ( x = ( 1st ` z ) -> ( x + 1 ) = ( ( 1st ` z ) + 1 ) )
65	64, 55	opeq12d 3816	. . . . . . . . . . . . . . . . 17 |- ( x = ( 1st ` z ) -> <. ( x + 1 ) , ( x F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. )
66	57	opeq2d 3815	. . . . . . . . . . . . . . . . 17 |- ( y = ( 2nd ` z ) -> <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F y ) >. = <. ( ( 1st ` z ) + 1 ) , ( ( 1st ` z ) F ( 2nd ` z ) ) >. )
67		eqid 2196	. . . . . . . . . . . . . . . . 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 6057	. . . . . . . . . . . . . . . 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 1249	. . . . . . . . . . . . . . 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 2243	. . . . . . . . . . . . . 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 2273	. . . . . . . . . . . . 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 2273	. . . . . . . . . . . 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 2570	. . . . . . . . . . 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 4693	. . . . . . . . . . . 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 6465	. . . . . . . . . . 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 1249	. . . . . . . . . 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 5559	. . . . . . . . . 10 |- ( R ` suc v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` suc v )
82	23	fveq1i 5559	. . . . . . . . . . 11 |- ( R ` v ) = (frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) ` v )
83	82	fveq2i 5561	. . . . . . . . . 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 2254	. . . . . . . . 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 5558	. . . . . . . . 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 5925	. . . . . . . . . 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 10494	. . . . . . . . . . 11 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ( ZZ>= ` C ) )
90	25, 32, 26, 52, 23	frecuzrdgrrn 10500	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( R ` v ) e. ( ( ZZ>= ` C ) X. S ) )
91		xp2nd 6224	. . . . . . . . . . . 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 9657	. . . . . . . . . . . . 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 6076	. . . . . . . . . . . . . 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 6077	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) e. S )
98		opelxp 4693	. . . . . . . . . . . 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 5929	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w + 1 ) = ( ( G ` v ) + 1 ) )
101		oveq1 5929	. . . . . . . . . . . . 13 |- ( w = ( G ` v ) -> ( w F z ) = ( ( G ` v ) F z ) )
102	100, 101	opeq12d 3816	. . . . . . . . . . . 12 |- ( w = ( G ` v ) -> <. ( w + 1 ) , ( w F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. )
103		oveq2 5930	. . . . . . . . . . . . 13 |- ( z = ( 2nd ` ( R ` v ) ) -> ( ( G ` v ) F z ) = ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) )
104	103	opeq2d 3815	. . . . . . . . . . . 12 |- ( z = ( 2nd ` ( R ` v ) ) -> <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F z ) >. = <. ( ( G ` v ) + 1 ) , ( ( G ` v ) F ( 2nd ` ( R ` v ) ) ) >. )
105		oveq1 5929	. . . . . . . . . . . . . 14 |- ( x = w -> ( x + 1 ) = ( w + 1 ) )
106		oveq1 5929	. . . . . . . . . . . . . 14 |- ( x = w -> ( x F y ) = ( w F y ) )
107	105, 106	opeq12d 3816	. . . . . . . . . . . . 13 |- ( x = w -> <. ( x + 1 ) , ( x F y ) >. = <. ( w + 1 ) , ( w F y ) >. )
108		oveq2 5930	. . . . . . . . . . . . . 14 |- ( y = z -> ( w F y ) = ( w F z ) )
109	108	opeq2d 3815	. . . . . . . . . . . . 13 |- ( y = z -> <. ( w + 1 ) , ( w F y ) >. = <. ( w + 1 ) , ( w F z ) >. )
110	107, 109	cbvmpov 6002	. . . . . . . . . . . 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 6057	. . . . . . . . . . 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 1249	. . . . . . . . . 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 2243	. . . . . . . . 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 2251	. . . . . . . 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 2229	. . . . . . 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 10493	. . . . . . . . 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 5562	. . . . . . . . 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 10492	. . . . . . . . . . . 12 |- ( ( ph /\ v e. om ) -> ( G ` v ) e. ZZ )
120	119	peano2zd 9451	. . . . . . . . . . 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 6209	. . . . . . . . . 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 2229	. . . . . . . 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 3816	. . . . . . 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 2232	. . . . . 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 4637	. . 3 |- ( z e. om -> ( ph -> ( R ` z ) = <. ( G ` z ) , ( 2nd ` ( R ` z ) ) >. ) )
131	7, 130	vtoclga 2830	. 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 1364   e. wcel 2167   A.wral 2475   _Vcvv 2763   (/)c0 3450   <.cop 3625   |-> cmpt 4094   suc csuc 4400   omcom 4626   X. cxp 4661   ` cfv 5258  (class class class)co 5922   e. cmpo 5924   1stc1st 6196   2ndc2nd 6197  freccfrec 6448   1c1 7880   + caddc 7882   ZZcz 9326   ZZ>=cuz 9601

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-ltadd 7995

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-n0 9250  df-z 9327  df-uz 9602

This theorem is referenced by:  frecuzrdglem  10503  frecuzrdgtcl  10504  frecuzrdgsuc  10506