Theorem tfr1

Description: Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of TakeutiZaring p. 47. We start with an arbitrary class G , normally a function, and define a class A of all "acceptable" functions. The final function we're interested in is the union F = recs ( G ) of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F . In this first part we show that F is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994) (Revised by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypothesis	tfr.1	$$⊢F=\mathrm{recs}\left(G\right)$$
Assertion	tfr1	$$⊢FFn\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$$⊢F=\mathrm{recs}\left(G\right)$$
2		eqid	$$⊢\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=G\left({f\upharpoonright }_y\right)\right)\right\}=\left\{f|\exists x\in \mathrm{On}\left(fFnx\wedge \forall y\in xf\left(y\right)=G\left({f\upharpoonright }_y\right)\right)\right\}$$
3	2	tfrlem7	$$⊢\mathrm{Fun}\mathrm{recs}\left(G\right)$$
4	2	tfrlem14	$$⊢\mathrm{dom}\mathrm{recs}\left(G\right)=\mathrm{On}$$
5		df-fn	$$⊢\mathrm{recs}\left(G\right)Fn\mathrm{On}\leftrightarrow \left(\mathrm{Fun}\mathrm{recs}\left(G\right)\wedge \mathrm{dom}\mathrm{recs}\left(G\right)=\mathrm{On}\right)$$
6	3 4 5	mpbir2an	$$⊢\mathrm{recs}\left(G\right)Fn\mathrm{On}$$
7	1	fneq1i	$$⊢FFn\mathrm{On}\leftrightarrow \mathrm{recs}\left(G\right)Fn\mathrm{On}$$
8	6 7	mpbir	$$⊢FFn\mathrm{On}$$