Theorem tfr2

Description: Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of TakeutiZaring p. 47. Here we show that the function F has the property that for any function G whatsoever, the "next" value of F is G recursively applied to all "previous" values of F . (Contributed by NM, 9-Apr-1995) (Revised by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypothesis	tfr.1	$$⊢F=\mathrm{recs}\left(G\right)$$
Assertion	tfr2	$$⊢A\in \mathrm{On}\to F\left(A\right)=G\left({F\upharpoonright }_A\right)$$

Proof

Step	Hyp	Ref	Expression
1		tfr.1	$$⊢F=\mathrm{recs}\left(G\right)$$
2	1	tfr1	$$⊢FFn\mathrm{On}$$
3	2	fndmi	$$⊢\mathrm{dom}F=\mathrm{On}$$
4	3	eleq2i	$$⊢A\in \mathrm{dom}F\leftrightarrow A\in \mathrm{On}$$
5	1	tfr2a	$$⊢A\in \mathrm{dom}F\to F\left(A\right)=G\left({F\upharpoonright }_A\right)$$
6	4 5	sylbir	$$⊢A\in \mathrm{On}\to F\left(A\right)=G\left({F\upharpoonright }_A\right)$$