Description: The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rdgfnon | |- rec ( F , A ) Fn On |
| 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 | tfr1 | |- rec ( F , A ) Fn On |