This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )