This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )