Metamath Proof Explorer


Theorem rdgvalg

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

Proof

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