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 On F A = G F A

Proof

Step Hyp Ref Expression
1 tfr.1 F = recs G
2 1 tfr1 F Fn On
3 fndm F Fn On dom F = On
4 2 3 ax-mp dom F = On
5 4 eleq2i A dom F A On
6 1 tfr2a A dom F F A = G F A
7 5 6 sylbir A On F A = G F A