Metamath Proof Explorer


Theorem rdgfnon

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 recFAFnOn

Proof

Step Hyp Ref Expression
1 df-rdg recFA=recsgVifg=AifLimdomgrangFgdomg
2 1 tfr1 recFAFnOn