Metamath Proof Explorer

Theorem rdgfun

Description: The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rdgfun 
|- Fun rec ( F , A )

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 tfr1a 
 |-  ( Fun rec ( F , A ) /\ Lim dom rec ( F , A ) )
3 2 simpli 
 |-  Fun rec ( F , A )