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


Step Hyp Ref Expression
1 tfr.1 F = recs G
2 eqid f | x On f Fn x y x f y = G f y = f | x On f Fn x y 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