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 = recs ( G )
Assertion	tfr2	|- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		tfr.1	|- F = recs ( G )
2	1	tfr1	|- F Fn On
3	2	fndmi	|- dom F = On
4	3	eleq2i	|- ( A e. dom F <-> A e. On )
5	1	tfr2a	|- ( A e. dom F -> ( F ` A ) = ( G ` ( F |` A ) ) )
6	4 5	sylbir	|- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )