Theorem rdgfun

Description: The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	rdgfun	⊢ Fun 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	simpli	⊢ Fun rec ( 𝐹 , 𝐴 )