Metamath Proof Explorer

Theorem rdgdmlim

Description: The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014)

Ref Expression
Assertion rdgdmlim 
|- Lim dom 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 simpri 
 |-  Lim dom rec ( F , A )