Metamath Proof Explorer

Theorem frsuc

Description: The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 16-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 rdgdmlim 
 |-  Lim dom rec ( F , A )
2 limomss 
 |-  ( Lim dom rec ( F , A ) -> _om C_ dom rec ( F , A ) )
3 1 2 ax-mp 
 |-  _om C_ dom rec ( F , A )
4 3 sseli 
 |-  ( B e. _om -> B e. dom rec ( F , A ) )
5 rdgsucg 
 |-  ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
6 4 5 syl 
 |-  ( B e. _om -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
7 peano2b 
 |-  ( B e. _om <-> suc B e. _om )
8 fvres 
 |-  ( suc B e. _om -> ( ( rec ( F , A ) |` _om ) ` suc B ) = ( rec ( F , A ) ` suc B ) )
9 7 8 sylbi 
 |-  ( B e. _om -> ( ( rec ( F , A ) |` _om ) ` suc B ) = ( rec ( F , A ) ` suc B ) )
10 fvres 
 |-  ( B e. _om -> ( ( rec ( F , A ) |` _om ) ` B ) = ( rec ( F , A ) ` B ) )
11 10 fveq2d 
 |-  ( B e. _om -> ( F ` ( ( rec ( F , A ) |` _om ) ` B ) ) = ( F ` ( rec ( F , A ) ` B ) ) )
12 6 9 11 3eqtr4d 
 |-  ( B e. _om -> ( ( rec ( F , A ) |` _om ) ` suc B ) = ( F ` ( ( rec ( F , A ) |` _om ) ` B ) ) )