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	$$⊢\mathrm{rec}\left(F,A\right)Fn\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		df-rdg	$$⊢\mathrm{rec}\left(F,A\right)=\mathrm{recs}\left(\left(g\in \mathrm{V}⟼if\left(g=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}g,\bigcup \mathrm{ran}g,F\left(g\left(\bigcup \mathrm{dom}g\right)\right)\right)\right)\right)\right)$$
2	1	tfr1	$$⊢\mathrm{rec}\left(F,A\right)Fn\mathrm{On}$$