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	⊢ rec ( 𝐹 , 𝐴 ) Fn On

Proof

Step	Hyp	Ref	Expression
1		df-rdg	⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
2	1	tfr1	⊢ rec ( 𝐹 , 𝐴 ) Fn On