Description: Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | rdgvalg | |- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` B ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rdg | |- rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |
|
2 | 1 | tfr2a | |- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` B ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` B ) ) ) |