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	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		rdgfun	$$⊢\mathrm{Fun}\mathrm{rec}\left(F,A\right)$$
2		funres	$$⊢\mathrm{Fun}\mathrm{rec}\left(F,A\right)\to \mathrm{Fun}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
4		dmres	$$⊢\mathrm{dom}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)=\mathrm{\omega }\cap \mathrm{dom}\mathrm{rec}\left(F,A\right)$$
5		rdgdmlim	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left(F,A\right)$$
6		limomss	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{rec}\left(F,A\right)\to \mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left(F,A\right)$$
7	5 6	ax-mp	$$⊢\mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left(F,A\right)$$
8		df-ss	$$⊢\mathrm{\omega }\subseteq \mathrm{dom}\mathrm{rec}\left(F,A\right)\leftrightarrow \mathrm{\omega }\cap \mathrm{dom}\mathrm{rec}\left(F,A\right)=\mathrm{\omega }$$
9	7 8	mpbi	$$⊢\mathrm{\omega }\cap \mathrm{dom}\mathrm{rec}\left(F,A\right)=\mathrm{\omega }$$
10	4 9	eqtri	$$⊢\mathrm{dom}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)=\mathrm{\omega }$$
11		df-fn	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\leftrightarrow \left(\mathrm{Fun}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\wedge \mathrm{dom}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)=\mathrm{\omega }\right)$$
12	3 10 11	mpbir2an	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$$