Metamath Proof Explorer

Theorem rdgsucg

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014)

Ref Expression
Assertion rdgsucg 
|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 rdgdmlim 
 |-  Lim dom rec ( F , A )
2 limsuc 
 |-  ( Lim dom rec ( F , A ) -> ( B e. dom rec ( F , A ) <-> suc B e. dom rec ( F , A ) ) )
3 1 2 ax-mp 
 |-  ( B e. dom rec ( F , A ) <-> suc B e. dom rec ( F , A ) )
4 eqid 
 |-  ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) )
5 rdgvalg 
 |-  ( y e. dom rec ( F , A ) -> ( rec ( F , A ) ` y ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` y ) ) )
6 rdgseg 
 |-  ( y e. dom rec ( F , A ) -> ( rec ( F , A ) |` y ) e. _V )
7 rdgfun 
 |-  Fun rec ( F , A )
8 funfn 
 |-  ( Fun rec ( F , A ) <-> rec ( F , A ) Fn dom rec ( F , A ) )
9 7 8 mpbi 
 |-  rec ( F , A ) Fn dom rec ( F , A )
10 limord 
 |-  ( Lim dom rec ( F , A ) -> Ord dom rec ( F , A ) )
11 1 10 ax-mp 
 |-  Ord dom rec ( F , A )
12 4 5 6 9 11 tz7.44-2 
 |-  ( suc B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
13 3 12 sylbi 
 |-  ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )