Theorem tfrlem16

Description: Lemma for finite recursion. Without assuming ax-rep , we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014)

	Ref	Expression
Hypothesis	tfrlem.1	$$⊢A=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_y\right)\right)\right\}$$
Assertion	tfrlem16	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$$⊢A=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=F\left({f\upharpoonright }_y\right)\right)\right\}$$
2	1	tfrlem8	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)$$
3		ordzsl	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)\leftrightarrow \left(\mathrm{dom}\mathrm{recs}\left(F\right)=\varnothing \vee \exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)\right)$$
4	2 3	mpbi	$$⊢\left(\mathrm{dom}\mathrm{recs}\left(F\right)=\varnothing \vee \exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)\right)$$
5		res0	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\varnothing }=\varnothing$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7	5 6	eqeltri	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\varnothing }\in \mathrm{V}$$
8		0elon	$$⊢\varnothing \in \mathrm{On}$$
9	1	tfrlem15	$$⊢\varnothing \in \mathrm{On}\to \left(\varnothing \in \mathrm{dom}\mathrm{recs}\left(F\right)\leftrightarrow {\mathrm{recs}\left(F\right)\upharpoonright }_{\varnothing }\in \mathrm{V}\right)$$
10	8 9	ax-mp	$$⊢\varnothing \in \mathrm{dom}\mathrm{recs}\left(F\right)\leftrightarrow {\mathrm{recs}\left(F\right)\upharpoonright }_{\varnothing }\in \mathrm{V}$$
11	7 10	mpbir	$$⊢\varnothing \in \mathrm{dom}\mathrm{recs}\left(F\right)$$
12	11	n0ii	$$⊢\neg \mathrm{dom}\mathrm{recs}\left(F\right)=\varnothing$$
13	12	pm2.21i	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)=\varnothing \to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$
14	1	tfrlem13	$$⊢\neg \mathrm{recs}\left(F\right)\in \mathrm{V}$$
15		simpr	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z$$
16		df-suc	$$⊢\mathrm{suc}z=z\cup \left\{z\right\}$$
17	15 16	eqtrdi	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to \mathrm{dom}\mathrm{recs}\left(F\right)=z\cup \left\{z\right\}$$
18	17	reseq2d	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to {\mathrm{recs}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{recs}\left(F\right)}={\mathrm{recs}\left(F\right)\upharpoonright }_{\left(z\cup \left\{z\right\}\right)}$$
19	1	tfrlem6	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)$$
20		resdm	$$⊢\mathrm{Rel}\mathrm{recs}\left(F\right)\to {\mathrm{recs}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{recs}\left(F\right)}=\mathrm{recs}\left(F\right)$$
21	19 20	ax-mp	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\mathrm{dom}\mathrm{recs}\left(F\right)}=\mathrm{recs}\left(F\right)$$
22		resundi	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\left(z\cup \left\{z\right\}\right)}=\left({\mathrm{recs}\left(F\right)\upharpoonright }_z\right)\cup \left({\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\right)$$
23	18 21 22	3eqtr3g	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to \mathrm{recs}\left(F\right)=\left({\mathrm{recs}\left(F\right)\upharpoonright }_z\right)\cup \left({\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\right)$$
24		vex	$$⊢z\in \mathrm{V}$$
25	24	sucid	$$⊢z\in \mathrm{suc}z$$
26	25 15	eleqtrrid	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to z\in \mathrm{dom}\mathrm{recs}\left(F\right)$$
27	1	tfrlem9a	$$⊢z\in \mathrm{dom}\mathrm{recs}\left(F\right)\to {\mathrm{recs}\left(F\right)\upharpoonright }_z\in \mathrm{V}$$
28	26 27	syl	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to {\mathrm{recs}\left(F\right)\upharpoonright }_z\in \mathrm{V}$$
29		snex	$$⊢\left\{⟨z,\mathrm{recs}\left(F\right)\left(z\right)⟩\right\}\in \mathrm{V}$$
30	1	tfrlem7	$$⊢\mathrm{Fun}\mathrm{recs}\left(F\right)$$
31		funressn	$$⊢\mathrm{Fun}\mathrm{recs}\left(F\right)\to {\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\subseteq \left\{⟨z,\mathrm{recs}\left(F\right)\left(z\right)⟩\right\}$$
32	30 31	ax-mp	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\subseteq \left\{⟨z,\mathrm{recs}\left(F\right)\left(z\right)⟩\right\}$$
33	29 32	ssexi	$$⊢{\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\in \mathrm{V}$$
34		unexg	$$⊢\left({\mathrm{recs}\left(F\right)\upharpoonright }_z\in \mathrm{V}\wedge {\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\in \mathrm{V}\right)\to \left({\mathrm{recs}\left(F\right)\upharpoonright }_z\right)\cup \left({\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\right)\in \mathrm{V}$$
35	28 33 34	sylancl	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to \left({\mathrm{recs}\left(F\right)\upharpoonright }_z\right)\cup \left({\mathrm{recs}\left(F\right)\upharpoonright }_{\left\{z\right\}}\right)\in \mathrm{V}$$
36	23 35	eqeltrd	$$⊢\left(z\in \mathrm{On}\wedge \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\right)\to \mathrm{recs}\left(F\right)\in \mathrm{V}$$
37	36	rexlimiva	$$⊢\exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\to \mathrm{recs}\left(F\right)\in \mathrm{V}$$
38	14 37	mto	$$⊢\neg \exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z$$
39	38	pm2.21i	$$⊢\exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$
40		id	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$
41	13 39 40	3jaoi	$$⊢\left(\mathrm{dom}\mathrm{recs}\left(F\right)=\varnothing \vee \exists z\in \mathrm{On}\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{suc}z\vee \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)\right)\to \mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$
42	4 41	ax-mp	$$⊢\mathrm{Lim}\mathrm{dom}\mathrm{recs}\left(F\right)$$