# Metamath Proof Explorer

## Theorem tfr1

Description: Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of TakeutiZaring p. 47. We start with an arbitrary class G , normally a function, and define a class A of all "acceptable" functions. The final function we're interested in is the union F = recs ( G ) of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F . In this first part we show that F is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994) (Revised by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypothesis tfr.1
`|- F = recs ( G )`
Assertion tfr1
`|- F Fn On`

### Proof

Step Hyp Ref Expression
1 tfr.1
` |-  F = recs ( G )`
2 eqid
` |-  { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }`
3 2 tfrlem7
` |-  Fun recs ( G )`
4 2 tfrlem14
` |-  dom recs ( G ) = On`
5 df-fn
` |-  ( recs ( G ) Fn On <-> ( Fun recs ( G ) /\ dom recs ( G ) = On ) )`
6 3 4 5 mpbir2an
` |-  recs ( G ) Fn On`
7 1 fneq1i
` |-  ( F Fn On <-> recs ( G ) Fn On )`
8 6 7 mpbir
` |-  F Fn On`