Theorem rdgdmlim

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

	Ref	Expression
Assertion	rdgdmlim	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left(F,A\right)$$

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	tfr1a	$$⊢\left(\mathrm{Fun}\mathrm{rec}\left(F,A\right)\wedge \mathrm{Lim}\mathrm{dom}\mathrm{rec}\left(F,A\right)\right)$$
3	2	simpri	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left(F,A\right)$$