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