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
Theorem	pwuninel 7001	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. See also pwuninel2 7000. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- -. ~P U. A e. A
Theorem	undefval 7002	Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 7004 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( S e. V -> ( Undef ` S ) = ~P U. S )
Theorem	undefnel2 7003	The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.)
|- ( S e. V -> -. ( Undef ` S ) e. S )
Theorem	undefnel 7004	The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.)
|- ( S e. V -> ( Undef ` S ) e/ S )
Theorem	undefne0 7005	The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018.)
|- ( S e. V -> ( Undef ` S ) =/= (/) )
2.4.13  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 7006*	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 7007*	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 7008*	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 7009*	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 7010*	A variant of onfununi 7009 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 7011*	A variant of onovuni 7010 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 7012*	There are no length om decreasing sequences in the ordinals. See also noinfep 8072 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 7013	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 7014*	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 7015*	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 7016*	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 7017*	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 7018	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )
Theorem	smodm 7019	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( Smo A -> Ord dom A )
Theorem	smores 7020	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 7021	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 7022	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 7023	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 7024	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 7025	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 7026	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 7027	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 7028	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 7029*	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 7030	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 7031	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 7032	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 7033	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 7034	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 7035	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 7036	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 7037	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 7038	Notation for a function defined by strong transfinite recursion.
class recs ( F )
Definition	df-recs 7039*	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 7073 for more details on why this definition is desirable. Unlike df-rdg 7073 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 7066 and recsval 7067 for the primary contract of this definition. EDITORIAL: there are several existing versions of this construction without the definition, notably in ordtype 7953, zorn2 8882, and dfac8alem 8406. (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 7040	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( F = G -> recs ( F ) = recs ( G ) )
Theorem	nfrecs 7041	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F/_ x F   =>    |- F/_ xrecs ( F )
Theorem	tfrlem1 7042*	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 7043*	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 7044*	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 7045*	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 7046*	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 7047*	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 7048*	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 7049*	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 7050*	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 7051*	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 7052*	Lemma for transfinite recursion. Without using ax-rep 4558, 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 7053*	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 7057, 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 7054*	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 7055*	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 7056*	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 7057*	Lemma for transfinite recursion. Assuming ax-rep 4558, 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 7058*	Lemma for transfinite recursion. Without assuming ax-rep 4558, 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 7059*	Lemma for finite recursion. Without assuming ax-rep 4558, 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 7060	A weak version of tfr1 7063 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 7061	A weak version of tfr2 7064 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 7062	Without assuming ax-rep 4558, 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 7063	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 7064	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 7065*	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 7066	Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- recs ( F ) Fn On
Theorem	recsval 7067	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 7068*	G is a function. Lemma for tz7.44-1 7069, tz7.44-2 7070, and tz7.44-3 7071. (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 7069*	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 7070*	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 7071*	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 7072	Extend class notation with the recursive definition generator, with characteristic function F and initial value I.
class rec ( F , I )
Definition	df-rdg 7073*	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 7063 and G in tz7.44-1 7069 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 7039 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 7158, from which we prove the recursive textbook definition as theorems oa0 7163, oasuc 7171, and oalim 7179 (with the help of theorems rdg0 7084, rdgsuc 7087, and rdglim2a 7096). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers om; see fr0g 7098 and frsuc 7099. 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 3940) 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 12072 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 12318 and integer powers df-exp 12131. 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 7074	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 7075	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 7076	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 7077	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 7078*	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 7079	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- Fun rec ( F , A )
Theorem	rdgdmlim 7080	The domain of the recursive definition generator is a limit ordinal. (Contributed by NM, 16-Nov-2014.)
|- Lim dom rec ( F , A )
Theorem	rdgfnon 7081	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 7082*	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 7083*	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 7084	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 7085	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 7086	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 7087	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 7088	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 7089	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 7090	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
|- ( A e. C -> ( rec ( F , A ) ` (/) ) = A )
Theorem	rdgsucmptf 7091	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 7092	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 7091 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 7093*	This version of rdgsucmpt 7094 avoids the not-free hypothesis of rdgsucmptf 7091 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 7094*	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 7095*	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 7096*	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 7097	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 7098	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 7099	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 7100	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 )