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)
|- { 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 ) ) ) }