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	⊢ 𝐹 = recs ( 𝐺 )
	Assertion	tfr2	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tfr.1	⊢ 𝐹 = recs ( 𝐺 )
2	1	tfr1	⊢ 𝐹 Fn On
3	2	fndmi	⊢ dom 𝐹 = On
4	3	eleq2i	⊢ ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ On )
5	1	tfr2a	⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )
6	4 5	sylbir	⊢ ( 𝐴 ∈ On → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝐴 ) ) )