# 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}=\mathrm{recs}\left({G}\right)$
Assertion tfr2 ${⊢}{A}\in \mathrm{On}\to {F}\left({A}\right)={G}\left({{F}↾}_{{A}}\right)$

### Proof

Step Hyp Ref Expression
1 tfr.1 ${⊢}{F}=\mathrm{recs}\left({G}\right)$
2 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
3 fndm ${⊢}{F}Fn\mathrm{On}\to \mathrm{dom}{F}=\mathrm{On}$
4 2 3 ax-mp ${⊢}\mathrm{dom}{F}=\mathrm{On}$
5 4 eleq2i ${⊢}{A}\in \mathrm{dom}{F}↔{A}\in \mathrm{On}$
6 1 tfr2a ${⊢}{A}\in \mathrm{dom}{F}\to {F}\left({A}\right)={G}\left({{F}↾}_{{A}}\right)$
7 5 6 sylbir ${⊢}{A}\in \mathrm{On}\to {F}\left({A}\right)={G}\left({{F}↾}_{{A}}\right)$