Metamath Proof Explorer


Theorem rdgsuc

Description: The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 rdgfnon
 |-  rec ( F , A ) Fn On
2 1 fndmi
 |-  dom rec ( F , A ) = On
3 2 eleq2i
 |-  ( B e. dom rec ( F , A ) <-> B e. On )
4 rdgsucg
 |-  ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
5 3 4 sylbir
 |-  ( B e. On -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )