Metamath Proof Explorer

Theorem om2uzsuci

Description: The value of G (see om2uz0i ) at a successor. (Contributed by NM, 3-Oct-2004) (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 )
Assertion om2uzsuci 
|- ( A e. _om -> ( G ` suc A ) = ( ( G ` A ) + 1 ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 
 |-  C e. ZZ
2 om2uz.2 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , C ) |` _om )
3 suceq 
 |-  ( z = A -> suc z = suc A )
4 3 fveq2d 
 |-  ( z = A -> ( G ` suc z ) = ( G ` suc A ) )
5 fveq2 
 |-  ( z = A -> ( G ` z ) = ( G ` A ) )
6 5 oveq1d 
 |-  ( z = A -> ( ( G ` z ) + 1 ) = ( ( G ` A ) + 1 ) )
7 4 6 eqeq12d 
 |-  ( z = A -> ( ( G ` suc z ) = ( ( G ` z ) + 1 ) <-> ( G ` suc A ) = ( ( G ` A ) + 1 ) ) )
8 ovex 
 |-  ( ( G ` z ) + 1 ) e. _V
9 oveq1 
 |-  ( y = x -> ( y + 1 ) = ( x + 1 ) )
10 oveq1 
 |-  ( y = ( G ` z ) -> ( y + 1 ) = ( ( G ` z ) + 1 ) )
11 2 9 10 frsucmpt2 
 |-  ( ( z e. _om /\ ( ( G ` z ) + 1 ) e. _V ) -> ( G ` suc z ) = ( ( G ` z ) + 1 ) )
12 8 11 mpan2 
 |-  ( z e. _om -> ( G ` suc z ) = ( ( G ` z ) + 1 ) )
13 7 12 vtoclga 
 |-  ( A e. _om -> ( G ` suc A ) = ( ( G ` A ) + 1 ) )