Theorem frfnom

Description: The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996) (Revised by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Assertion	frfnom	⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω

Proof

Step	Hyp	Ref	Expression
1		rdgfun	⊢ Fun rec ( 𝐹 , 𝐴 )
2		funres	⊢ ( Fun rec ( 𝐹 , 𝐴 ) → Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
3	1 2	ax-mp	⊢ Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω )
4		dmres	⊢ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ( ω ∩ dom rec ( 𝐹 , 𝐴 ) )
5		rdgdmlim	⊢ Lim dom rec ( 𝐹 , 𝐴 )
6		limomss	⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → ω ⊆ dom rec ( 𝐹 , 𝐴 ) )
7	5 6	ax-mp	⊢ ω ⊆ dom rec ( 𝐹 , 𝐴 )
8		dfss2	⊢ ( ω ⊆ dom rec ( 𝐹 , 𝐴 ) ↔ ( ω ∩ dom rec ( 𝐹 , 𝐴 ) ) = ω )
9	7 8	mpbi	⊢ ( ω ∩ dom rec ( 𝐹 , 𝐴 ) ) = ω
10	4 9	eqtri	⊢ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ω
11		df-fn	⊢ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω ↔ ( Fun ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ∧ dom ( rec ( 𝐹 , 𝐴 ) ↾ ω ) = ω ) )
12	3 10 11	mpbir2an	⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω