P. 71 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
2.4.13  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 7001*	The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.)
|- ( ( A e. V /\ A. x e. A B e. On ) -> U_ x e. A B e. On )
Theorem	iunonOLD 7002*	The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A. x e. A B e. On -> U_ x e. A B e. On )
Theorem	iinon 7003*	The nonempty indexed intersection of a class of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ( A. x e. A B e. On /\ A =/= (/) ) -> |^|_ x e. A B e. On )
Theorem	onfununi 7004*	A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of [Enderton] p. 218. (Contributed by Eric Schmidt, 26-May-2009.)
|- ( Lim y -> ( F ` y ) = U_ x e. y ( F ` x ) )   &    |- ( ( x e. On /\ y e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) )   =>    |- ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( F ` U. S ) = U_ x e. S ( F ` x ) )
Theorem	onovuni 7005*	A variant of onfununi 7004 for operations. (Contributed by Eric Schmidt, 26-May-2009.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- ( Lim y -> ( A F y ) = U_ x e. y ( A F x ) )   &    |- ( ( x e. On /\ y e. On /\ x C_ y ) -> ( A F x ) C_ ( A F y ) )   =>    |- ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( A F U. S ) = U_ x e. S ( A F x ) )
Theorem	onoviun 7006*	A variant of onovuni 7005 with indexed unions. (Contributed by Eric Schmidt, 26-May-2009.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( Lim y -> ( A F y ) = U_ x e. y ( A F x ) )   &    |- ( ( x e. On /\ y e. On /\ x C_ y ) -> ( A F x ) C_ ( A F y ) )   =>    |- ( ( K e. T /\ A. z e. K L e. On /\ K =/= (/) ) -> ( A F U_ z e. K L ) = U_ z e. K ( A F L ) )
Theorem	onnseq 7007*	There are no length om decreasing sequences in the ordinals. See also noinfep 8067 for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015.)
|- ( ( F ` (/) ) e. On -> E. x e. om -. ( F ` suc x ) e. ( F ` x ) )
Syntax	wsmo 7008	Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.
wff Smo A
Definition	df-smo 7009*	Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.)
|- ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
Theorem	dfsmo2 7010*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) )
Theorem	issmo 7011*	Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.)
|- A : B --> On   &    |- Ord B   &    |- ( ( x e. B /\ y e. B ) -> ( x e. y -> ( A ` x ) e. ( A ` y ) ) )   &    |- dom A = B   =>    |- Smo A
Theorem	issmo2 7012*	Alternative definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( F : A --> B -> ( ( B C_ On /\ Ord A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) ) -> Smo F ) )
Theorem	smoeq 7013	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )
Theorem	smodm 7014	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( Smo A -> Ord dom A )
Theorem	smores 7015	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ( Smo A /\ B e. dom A ) -> Smo ( A |` B ) )
Theorem	smores3 7016	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
|- ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) /\ Ord B ) -> Smo ( A |` C ) )
Theorem	smores2 7017	A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
|- ( ( Smo F /\ Ord A ) -> Smo ( F |` A ) )
Theorem	smodm2 7018	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( ( F Fn A /\ Smo F ) -> Ord A )
Theorem	smofvon2 7019	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( Smo F -> ( F ` B ) e. On )
Theorem	iordsmo 7020	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- Ord A   =>    |- Smo ( _I |` A )
Theorem	smo0 7021	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 7022	If B is a strictly monotone ordinal function, and A is in the domain of B, then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- ( ( Smo B /\ A e. dom B ) -> ( B ` A ) e. On )
Theorem	smoel 7023	If x is less than y then a strictly monotone function's value will be strictly less at x than at y. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ( ( Smo B /\ A e. dom B /\ C e. A ) -> ( B ` C ) e. ( B ` A ) )
Theorem	smoiun 7024*	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ( ( Smo B /\ A e. dom B ) -> U_ x e. A ( B ` x ) C_ ( B ` A ) )
Theorem	smoiso 7025	If F is an isomorphism from an ordinal A onto B, which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F )
Theorem	smoel2 7026	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( ( ( F Fn A /\ Smo F ) /\ ( B e. A /\ C e. B ) ) -> ( F ` C ) e. ( F ` B ) )
Theorem	smo11 7027	A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( ( F : A --> B /\ Smo F ) -> F : A -1-1-> B )
Theorem	smoord 7028	A strictly monotone ordinal function preserves strict ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( C e. D <-> ( F ` C ) e. ( F ` D ) ) )
Theorem	smoword 7029	A strictly monotone ordinal function preserves weak ordering. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- ( ( ( F Fn A /\ Smo F ) /\ ( C e. A /\ D e. A ) ) -> ( C C_ D <-> ( F ` C ) C_ ( F ` D ) ) )
Theorem	smogt 7030	A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 23-Nov-2011.) (Revised by Mario Carneiro, 28-Feb-2013.)
|- ( ( F Fn A /\ Smo F /\ C e. A ) -> C C_ ( F ` C ) )
Theorem	smorndom 7031	The range of a strictly monotone ordinal function dominates the domain. (Contributed by Mario Carneiro, 13-Mar-2013.)
|- ( ( F : A --> B /\ Smo F /\ Ord B ) -> A C_ B )
Theorem	smoiso2 7032	The strictly monotone ordinal functions are also epsilon isomorphisms of subclasses of On. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- ( ( Ord A /\ B C_ On ) -> ( ( F : A -onto-> B /\ Smo F ) <-> F Isom _E , _E ( A , B ) ) )
2.4.14  "Strong" transfinite recursion
Syntax	crecs 7033	Notation for a function defined by strong transfinite recursion.
class recs ( F )
Definition	df-recs 7034*	Define a function recs ( F ) on On, the class of ordinal numbers, by transfinite recursion given a rule F which sets the next value given all values so far. See df-rdg 7068 for more details on why this definition is desirable. Unlike df-rdg 7068 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See recsfnon 7061 and recsval 7062 for the primary contract of this definition. EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7949, zorn2 8877, and dfac8alem 8401. (Contributed by Stefan O'Rear, 18-Jan-2015.) (New usage is discouraged.)
|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Theorem	recseq 7035	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( F = G -> recs ( F ) = recs ( G ) )
Theorem	nfrecs 7036	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F/_ x F   =>    |- F/_ xrecs ( F )
Theorem	tfrlem1 7037*	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
|- ( ph -> A e. On )   &    |- ( ph -> ( Fun F /\ A C_ dom F ) )   &    |- ( ph -> ( Fun G /\ A C_ dom G ) )   &    |- ( ph -> A. x e. A ( F ` x ) = ( B ` ( F |` x ) ) )   &    |- ( ph -> A. x e. A ( G ` x ) = ( B ` ( G |` x ) ) )   =>    |- ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )
Theorem	tfrlem3a 7038*	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- G e. _V   =>    |- ( G e. A <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) )
Theorem	tfrlem3 7039*	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- A = { g | E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) }
Theorem	tfrlem4 7040*	Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( g e. A -> Fun g )
Theorem	tfrlem5 7041*	Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )
Theorem	recsfval 7042*	Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- recs ( F ) = U. A
Theorem	tfrlem6 7043*	Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Rel recs ( F )
Theorem	tfrlem7 7044*	Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Fun recs ( F )
Theorem	tfrlem8 7045*	Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Ord dom recs ( F )
Theorem	tfrlem9 7046*	Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( B e. dom recs ( F ) -> (recs ( F ) ` B ) = ( F ` (recs ( F ) |` B ) ) )
Theorem	tfrlem9a 7047*	Lemma for transfinite recursion. Without using ax-rep 4550, show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( B e. dom recs ( F ) -> (recs ( F ) |` B ) e. _V )
Theorem	tfrlem10 7048*	Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On. Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 7052, thus showing the domain of recs does in fact equal On. Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- C = (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )   =>    |- ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )
Theorem	tfrlem11 7049*	Lemma for transfinite recursion. Compute the value of C. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- C = (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )   =>    |- ( dom recs ( F ) e. On -> ( B e. suc dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
Theorem	tfrlem12 7050*	Lemma for transfinite recursion. Show C is an acceptable function. (Contributed by NM, 15-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- C = (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )   =>    |- (recs ( F ) e. _V -> C e. A )
Theorem	tfrlem13 7051*	Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs, but dom C is bigger than dom recs. This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- -. recs ( F ) e. _V
Theorem	tfrlem14 7052*	Lemma for transfinite recursion. Assuming ax-rep 4550, dom recs e. _V <-> recs e. _V, so since dom recs is an ordinal, it must be equal to On. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- dom recs ( F ) = On
Theorem	tfrlem15 7053*	Lemma for transfinite recursion. Without assuming ax-rep 4550, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( B e. On -> ( B e. dom recs ( F ) <-> (recs ( F ) |` B ) e. _V ) )
Theorem	tfrlem16 7054*	Lemma for finite recursion. Without assuming ax-rep 4550, we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Lim dom recs ( F )
Theorem	tfr1a 7055	A weak version of tfr1 7058 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- F = recs ( G )   =>    |- ( Fun F /\ Lim dom F )
Theorem	tfr2a 7056	A weak version of tfr2 7059 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- F = recs ( G )   =>    |- ( A e. dom F -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfr2b 7057	Without assuming ax-rep 4550, we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- F = recs ( G )   =>    |- ( Ord A -> ( A e. dom F <-> ( F |` A ) e. _V ) )
Theorem	tfr1 7058	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 = recs ( G )   =>    |- F Fn On
Theorem	tfr2 7059	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.)
|- F = recs ( G )   =>    |- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfr3 7060*	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47. Finally, we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
|- F = recs ( G )   =>    |- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )
Theorem	recsfnon 7061	Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- recs ( F ) Fn On
Theorem	recsval 7062	Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( A e. On -> (recs ( F ) ` A ) = ( F ` (recs ( F ) |` A ) ) )
Theorem	tz7.44lem1 7063*	G is a function. Lemma for tz7.44-1 7064, tz7.44-2 7065, and tz7.44-3 7066. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- G = { <. x , y >. | ( ( x = (/) /\ y = A ) \/ ( -. ( x = (/) \/ Lim dom x ) /\ y = ( H ` ( x ` U. dom x ) ) ) \/ ( Lim dom x /\ y = U. ran x ) ) }   =>    |- Fun G
Theorem	tz7.44-1 7064*	The value of F at (/). Part 1 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )   &    |- ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )   &    |- A e. _V   =>    |- ( (/) e. X -> ( F ` (/) ) = A )
Theorem	tz7.44-2 7065*	The value of F at a successor ordinal. Part 2 of Theorem 7.44 of [TakeutiZaring] p. 49. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )   &    |- ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )   &    |- ( y e. X -> ( F |` y ) e. _V )   &    |- F Fn X   &    |- Ord X   =>    |- ( suc B e. X -> ( F ` suc B ) = ( H ` ( F ` B ) ) )
Theorem	tz7.44-3 7066*	The value of F at a limit ordinal. Part 3 of Theorem 7.44 of [TakeutiZaring] p. 49. (Contributed by NM, 23-Apr-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )   &    |- ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )   &    |- ( y e. X -> ( F |` y ) e. _V )   &    |- F Fn X   &    |- Ord X   =>    |- ( ( B e. X /\ Lim B ) -> ( F ` B ) = U. ( F " B ) )
2.4.15  Recursive definition generator
Syntax	crdg 7067	Extend class notation with the recursive definition generator, with characteristic function F and initial value I.
class rec ( F , I )
Definition	df-rdg 7068*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function F and initial value I. This combines functions F in tfr1 7058 and G in tz7.44-1 7064 into one definition. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our rec operation (especially when df-recs 7034 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple, as in for example oav 7153, from which we prove the recursive textbook definition as theorems oa0 7158, oasuc 7166, and oalim 7174 (with the help of theorems rdg0 7079, rdgsuc 7082, and rdglim2a 7091). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers om; see fr0g 7093 and frsuc 7094. Our rec operation apparently does not appear in published literature, although closely related is Definition 25.2 of [Quine] p. 177, which he uses to "turn...a recursion into a genuine or direct definition" (p. 174). Note that the if operations (see df-if 3930) select cases based on whether the domain of g is zero, a successor, or a limit ordinal. An important use of this definition is in the recursive sequence generator df-seq 12090 on the natural numbers (as a subset of the complex numbers), allowing us to define, with direct definitions, recursive infinite sequences such as the factorial function df-fac 12336 and integer powers df-exp 12149. Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- rec ( F , I ) = recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
Theorem	rdgeq1 7069	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- ( F = G -> rec ( F , A ) = rec ( G , A ) )
Theorem	rdgeq2 7070	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- ( A = B -> rec ( F , A ) = rec ( F , B ) )
Theorem	rdgeq12 7071	Equality theorem for the recursive definition generator. (Contributed by Scott Fenton, 28-Apr-2012.)
|- ( ( F = G /\ A = B ) -> rec ( F , A ) = rec ( G , B ) )
Theorem	nfrdg 7072	Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/_ x rec ( F , A )
Theorem	rdglem1 7073*	Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. (Contributed by NM, 9-Apr-1995.)
|- { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { g | E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) }
Theorem	rdgfun 7074	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- Fun rec ( F , A )
Theorem	rdgdmlim 7075	The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)
|- Lim dom rec ( F , A )
Theorem	rdgfnon 7076	The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- rec ( F , A ) Fn On
Theorem	rdgvalg 7077*	Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` B ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` B ) ) )
Theorem	rdgval 7078*	Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( B e. On -> ( rec ( F , A ) ` B ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` B ) ) )
Theorem	rdg0 7079	The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- A e. _V   =>    |- ( rec ( F , A ) ` (/) ) = A
Theorem	rdgseg 7080	The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) |` B ) e. _V )
Theorem	rdgsucg 7081	The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.)
|- ( B e. dom rec ( F , A ) -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
Theorem	rdgsuc 7082	The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( B e. On -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
Theorem	rdglimg 7083	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.)
|- ( ( B e. dom rec ( F , A ) /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )
Theorem	rdglim 7084	The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) )
Theorem	rdg0g 7085	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
|- ( A e. C -> ( rec ( F , A ) ` (/) ) = A )
Theorem	rdgsucmptf 7086	The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x D   &    |- F = rec ( ( x e. _V |-> C ) , A )   &    |- ( x = ( F ` B ) -> C = D )   =>    |- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )
Theorem	rdgsucmptnf 7087	The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with rdgsucmptf 7086 to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x D   &    |- F = rec ( ( x e. _V |-> C ) , A )   &    |- ( x = ( F ` B ) -> C = D )   =>    |- ( -. D e. _V -> ( F ` suc B ) = (/) )
Theorem	rdgsucmpt2 7088*	This version of rdgsucmpt 7089 avoids the not-free hypothesis of rdgsucmptf 7086 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- F = rec ( ( x e. _V |-> C ) , A )   &    |- ( y = x -> E = C )   &    |- ( y = ( F ` B ) -> E = D )   =>    |- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )
Theorem	rdgsucmpt 7089*	The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013.)
|- F = rec ( ( x e. _V |-> C ) , A )   &    |- ( x = ( F ` B ) -> C = D )   =>    |- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )
Theorem	rdglim2 7090*	The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995.)
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } )
Theorem	rdglim2a 7091*	The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998.)
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U_ x e. B ( rec ( F , A ) ` x ) )
2.4.16  Finite recursion
Theorem	frfnom 7092	The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( rec ( F , A ) |` om ) Fn om
Theorem	fr0g 7093	The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.)
|- ( A e. B -> ( ( rec ( F , A ) |` om ) ` (/) ) = A )
Theorem	frsuc 7094	The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( B e. om -> ( ( rec ( F , A ) |` om ) ` suc B ) = ( F ` ( ( rec ( F , A ) |` om ) ` B ) ) )
Theorem	frsucmpt 7095	The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003.) (Revised by Scott Fenton, 2-Nov-2011.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x D   &    |- F = ( rec ( ( x e. _V |-> C ) , A ) |` om )   &    |- ( x = ( F ` B ) -> C = D )   =>    |- ( ( B e. om /\ D e. V ) -> ( F ` suc B ) = D )
Theorem	frsucmptn 7096	The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with frsucmpt 7095 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x D   &    |- F = ( rec ( ( x e. _V |-> C ) , A ) |` om )   &    |- ( x = ( F ` B ) -> C = D )   =>    |- ( -. D e. _V -> ( F ` suc B ) = (/) )
Theorem	frsucmpt2 7097*	The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- F = ( rec ( ( x e. _V |-> C ) , A ) |` om )   &    |- ( y = x -> E = C )   &    |- ( y = ( F ` B ) -> E = D )   =>    |- ( ( B e. om /\ D e. V ) -> ( F ` suc B ) = D )
Theorem	tz7.48lem 7098*	A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.)
|- F Fn On   =>    |- ( ( A C_ On /\ A. x e. A A. y e. x -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` A ) )
Theorem	tz7.48-2 7099*	Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.)
|- F Fn On   =>    |- ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> Fun `' F )
Theorem	tz7.48-1 7100*	Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.)
|- F Fn On   =>    |- ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ran F C_ A )