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 ( F , A ) |` _om ) Fn _om

Proof

Step	Hyp	Ref	Expression
1		rdgfun	|- Fun rec ( F , A )
2		funres	|- ( Fun rec ( F , A ) -> Fun ( rec ( F , A ) |` _om ) )
3	1 2	ax-mp	|- Fun ( rec ( F , A ) |` _om )
4		dmres	|- dom ( rec ( F , A ) |` _om ) = ( _om i^i dom rec ( F , A ) )
5		rdgdmlim	|- Lim dom rec ( F , A )
6		limomss	|- ( Lim dom rec ( F , A ) -> _om C_ dom rec ( F , A ) )
7	5 6	ax-mp	|- _om C_ dom rec ( F , A )
8		df-ss	|- ( _om C_ dom rec ( F , A ) <-> ( _om i^i dom rec ( F , A ) ) = _om )
9	7 8	mpbi	|- ( _om i^i dom rec ( F , A ) ) = _om
10	4 9	eqtri	|- dom ( rec ( F , A ) |` _om ) = _om
11		df-fn	|- ( ( rec ( F , A ) |` _om ) Fn _om <-> ( Fun ( rec ( F , A ) |` _om ) /\ dom ( rec ( F , A ) |` _om ) = _om ) )
12	3 10 11	mpbir2an	|- ( rec ( F , A ) |` _om ) Fn _om