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

Step

Hyp

Ref

Expression

df-rdg

 |-  rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )

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