Theorem uzrdgsuci

Description: Successor value of a recursive definition generator on upper integers. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	|- C e. ZZ
	om2uz.2	|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
	uzrdg.1	|- A e. _V
	uzrdg.2	|- R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
	uzrdg.3	|- S = ran R
Assertion	uzrdgsuci	|- ( B e. ( ZZ>= ` C ) -> ( S ` ( B + 1 ) ) = ( B F ( S ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	|- C e. ZZ
2		om2uz.2	|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3		uzrdg.1	|- A e. _V
4		uzrdg.2	|- R = ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om )
5		uzrdg.3	|- S = ran R
6	1 2 3 4 5	uzrdgfni	|- S Fn ( ZZ>= ` C )
7		fnfun	|- ( S Fn ( ZZ>= ` C ) -> Fun S )
8	6 7	ax-mp	|- Fun S
9		peano2uz	|- ( B e. ( ZZ>= ` C ) -> ( B + 1 ) e. ( ZZ>= ` C ) )
10	1 2 3 4	uzrdglem	|- ( ( B + 1 ) e. ( ZZ>= ` C ) -> <. ( B + 1 ) , ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) >. e. ran R )
11	9 10	syl	|- ( B e. ( ZZ>= ` C ) -> <. ( B + 1 ) , ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) >. e. ran R )
12	11 5	eleqtrrdi	|- ( B e. ( ZZ>= ` C ) -> <. ( B + 1 ) , ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) >. e. S )
13		funopfv	|- ( Fun S -> ( <. ( B + 1 ) , ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) >. e. S -> ( S ` ( B + 1 ) ) = ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) ) )
14	8 12 13	mpsyl	|- ( B e. ( ZZ>= ` C ) -> ( S ` ( B + 1 ) ) = ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) )
15	1 2	om2uzf1oi	|- G : _om -1-1-onto-> ( ZZ>= ` C )
16		f1ocnvdm	|- ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ B e. ( ZZ>= ` C ) ) -> ( `' G ` B ) e. _om )
17	15 16	mpan	|- ( B e. ( ZZ>= ` C ) -> ( `' G ` B ) e. _om )
18		peano2	|- ( ( `' G ` B ) e. _om -> suc ( `' G ` B ) e. _om )
19	17 18	syl	|- ( B e. ( ZZ>= ` C ) -> suc ( `' G ` B ) e. _om )
20	1 2	om2uzsuci	|- ( ( `' G ` B ) e. _om -> ( G ` suc ( `' G ` B ) ) = ( ( G ` ( `' G ` B ) ) + 1 ) )
21	17 20	syl	|- ( B e. ( ZZ>= ` C ) -> ( G ` suc ( `' G ` B ) ) = ( ( G ` ( `' G ` B ) ) + 1 ) )
22		f1ocnvfv2	|- ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ B e. ( ZZ>= ` C ) ) -> ( G ` ( `' G ` B ) ) = B )
23	15 22	mpan	|- ( B e. ( ZZ>= ` C ) -> ( G ` ( `' G ` B ) ) = B )
24	23	oveq1d	|- ( B e. ( ZZ>= ` C ) -> ( ( G ` ( `' G ` B ) ) + 1 ) = ( B + 1 ) )
25	21 24	eqtrd	|- ( B e. ( ZZ>= ` C ) -> ( G ` suc ( `' G ` B ) ) = ( B + 1 ) )
26		f1ocnvfv	|- ( ( G : _om -1-1-onto-> ( ZZ>= ` C ) /\ suc ( `' G ` B ) e. _om ) -> ( ( G ` suc ( `' G ` B ) ) = ( B + 1 ) -> ( `' G ` ( B + 1 ) ) = suc ( `' G ` B ) ) )
27	15 26	mpan	|- ( suc ( `' G ` B ) e. _om -> ( ( G ` suc ( `' G ` B ) ) = ( B + 1 ) -> ( `' G ` ( B + 1 ) ) = suc ( `' G ` B ) ) )
28	19 25 27	sylc	|- ( B e. ( ZZ>= ` C ) -> ( `' G ` ( B + 1 ) ) = suc ( `' G ` B ) )
29	28	fveq2d	|- ( B e. ( ZZ>= ` C ) -> ( R ` ( `' G ` ( B + 1 ) ) ) = ( R ` suc ( `' G ` B ) ) )
30	29	fveq2d	|- ( B e. ( ZZ>= ` C ) -> ( 2nd ` ( R ` ( `' G ` ( B + 1 ) ) ) ) = ( 2nd ` ( R ` suc ( `' G ` B ) ) ) )
31	14 30	eqtrd	|- ( B e. ( ZZ>= ` C ) -> ( S ` ( B + 1 ) ) = ( 2nd ` ( R ` suc ( `' G ` B ) ) ) )
32		frsuc	|- ( ( `' G ` B ) e. _om -> ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) ) )
33	4	fveq1i	|- ( R ` suc ( `' G ` B ) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` suc ( `' G ` B ) )
34	4	fveq1i	|- ( R ` ( `' G ` B ) ) = ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) )
35	34	fveq2i	|- ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( ( rec ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. ) |` _om ) ` ( `' G ` B ) ) )
36	32 33 35	3eqtr4g	|- ( ( `' G ` B ) e. _om -> ( R ` suc ( `' G ` B ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) )
37	1 2 3 4	om2uzrdg	|- ( ( `' G ` B ) e. _om -> ( R ` ( `' G ` B ) ) = <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
38	37	fveq2d	|- ( ( `' G ` B ) e. _om -> ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. ) )
39		df-ov	|- ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` <. ( G ` ( `' G ` B ) ) , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. )
40	38 39	eqtr4di	|- ( ( `' G ` B ) e. _om -> ( ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ` ( R ` ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
41	36 40	eqtrd	|- ( ( `' G ` B ) e. _om -> ( R ` suc ( `' G ` B ) ) = ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
42		fvex	|- ( G ` ( `' G ` B ) ) e. _V
43		fvex	|- ( 2nd ` ( R ` ( `' G ` B ) ) ) e. _V
44		oveq1	|- ( z = ( G ` ( `' G ` B ) ) -> ( z + 1 ) = ( ( G ` ( `' G ` B ) ) + 1 ) )
45		oveq1	|- ( z = ( G ` ( `' G ` B ) ) -> ( z F w ) = ( ( G ` ( `' G ` B ) ) F w ) )
46	44 45	opeq12d	|- ( z = ( G ` ( `' G ` B ) ) -> <. ( z + 1 ) , ( z F w ) >. = <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F w ) >. )
47		oveq2	|- ( w = ( 2nd ` ( R ` ( `' G ` B ) ) ) -> ( ( G ` ( `' G ` B ) ) F w ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
48	47	opeq2d	|- ( w = ( 2nd ` ( R ` ( `' G ` B ) ) ) -> <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F w ) >. = <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
49		oveq1	|- ( x = z -> ( x + 1 ) = ( z + 1 ) )
50		oveq1	|- ( x = z -> ( x F y ) = ( z F y ) )
51	49 50	opeq12d	|- ( x = z -> <. ( x + 1 ) , ( x F y ) >. = <. ( z + 1 ) , ( z F y ) >. )
52		oveq2	|- ( y = w -> ( z F y ) = ( z F w ) )
53	52	opeq2d	|- ( y = w -> <. ( z + 1 ) , ( z F y ) >. = <. ( z + 1 ) , ( z F w ) >. )
54	51 53	cbvmpov	|- ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) = ( z e. _V , w e. _V |-> <. ( z + 1 ) , ( z F w ) >. )
55		opex	|- <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. e. _V
56	46 48 54 55	ovmpo	|- ( ( ( G ` ( `' G ` B ) ) e. _V /\ ( 2nd ` ( R ` ( `' G ` B ) ) ) e. _V ) -> ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
57	42 43 56	mp2an	|- ( ( G ` ( `' G ` B ) ) ( x e. _V , y e. _V |-> <. ( x + 1 ) , ( x F y ) >. ) ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >.
58	41 57	eqtrdi	|- ( ( `' G ` B ) e. _om -> ( R ` suc ( `' G ` B ) ) = <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. )
59	58	fveq2d	|- ( ( `' G ` B ) e. _om -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( 2nd ` <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. ) )
60		ovex	|- ( ( G ` ( `' G ` B ) ) + 1 ) e. _V
61		ovex	|- ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) e. _V
62	60 61	op2nd	|- ( 2nd ` <. ( ( G ` ( `' G ` B ) ) + 1 ) , ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) >. ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) )
63	59 62	eqtrdi	|- ( ( `' G ` B ) e. _om -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
64	17 63	syl	|- ( B e. ( ZZ>= ` C ) -> ( 2nd ` ( R ` suc ( `' G ` B ) ) ) = ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
65	1 2 3 4	uzrdglem	|- ( B e. ( ZZ>= ` C ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. ran R )
66	65 5	eleqtrrdi	|- ( B e. ( ZZ>= ` C ) -> <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. S )
67		funopfv	|- ( Fun S -> ( <. B , ( 2nd ` ( R ` ( `' G ` B ) ) ) >. e. S -> ( S ` B ) = ( 2nd ` ( R ` ( `' G ` B ) ) ) ) )
68	8 66 67	mpsyl	|- ( B e. ( ZZ>= ` C ) -> ( S ` B ) = ( 2nd ` ( R ` ( `' G ` B ) ) ) )
69	68	eqcomd	|- ( B e. ( ZZ>= ` C ) -> ( 2nd ` ( R ` ( `' G ` B ) ) ) = ( S ` B ) )
70	23 69	oveq12d	|- ( B e. ( ZZ>= ` C ) -> ( ( G ` ( `' G ` B ) ) F ( 2nd ` ( R ` ( `' G ` B ) ) ) ) = ( B F ( S ` B ) ) )
71	31 64 70	3eqtrd	|- ( B e. ( ZZ>= ` C ) -> ( S ` ( B + 1 ) ) = ( B F ( S ` B ) ) )