Theorem rdgdmlim

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

	Ref	Expression
Assertion	rdgdmlim	⊢ Lim dom rec ( 𝐹 , 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-rdg	⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
2	1	tfr1a	⊢ ( Fun rec ( 𝐹 , 𝐴 ) ∧ Lim dom rec ( 𝐹 , 𝐴 ) )
3	2	simpri	⊢ Lim dom rec ( 𝐹 , 𝐴 )