Theorem tfrlem14

Description: Lemma for transfinite recursion. Assuming ax-rep , dom recs e.V <-> recs e. V , so since dom recs is an ordinal, it must be equal to On . (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

	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	tfrlem14	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{On}$$

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	tfrlem13	$$⊢\neg \mathrm{recs}\left(F\right)\in \mathrm{V}$$
3	1	tfrlem7	$$⊢\mathrm{Fun}\mathrm{recs}\left(F\right)$$
4		funex	$$⊢\left(\mathrm{Fun}\mathrm{recs}\left(F\right)\wedge \mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\right)\to \mathrm{recs}\left(F\right)\in \mathrm{V}$$
5	3 4	mpan	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\to \mathrm{recs}\left(F\right)\in \mathrm{V}$$
6	2 5	mto	$$⊢\neg \mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}$$
7	1	tfrlem8	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)$$
8		ordeleqon	$$⊢\mathrm{Ord}\mathrm{dom}\mathrm{recs}\left(F\right)\leftrightarrow \left(\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\vee \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{On}\right)$$
9	7 8	mpbi	$$⊢\left(\mathrm{dom}\mathrm{recs}\left(F\right)\in \mathrm{On}\vee \mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{On}\right)$$
10	6 9	mtpor	$$⊢\mathrm{dom}\mathrm{recs}\left(F\right)=\mathrm{On}$$