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