P. 75 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pwuninel 7401	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 7400. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- -. ~P U. A e. A
Theorem	undefval 7402	Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 7404 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( S e. V -> ( Undef ` S ) = ~P U. S )
Theorem	undefnel2 7403	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 7404	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 7405	The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018.)
|- ( S e. V -> ( Undef ` S ) =/= (/) )
2.4.13  Well-founded recursion
Syntax	cwrecs 7406	Declare syntax for the well-founded recursive function generator.
class wrecs ( R , A , F )
Definition	df-wrecs 7407*	Here we define the well-founded recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function F, a relationship R, and a base set A, this definition generates a function G = wrecs ( R , A , F ) that has property that, at any point x e. A, ( G ` x ) = ( F ` ( G | ` Pred ( R , A , x ) ) ). See wfr1 7433, wfr2 7434, and wfr3 7435. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.)
|- wrecs ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
Theorem	wrecseq123 7408	General equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
|- ( ( R = S /\ A = B /\ F = G ) -> wrecs ( R , A , F ) = wrecs ( S , B , G ) )
Theorem	nfwrecs 7409	Bound-variable hypothesis builder for the well-founded recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.)
|- F/_ x R   &    |- F/_ x A   &    |- F/_ x F   =>    |- F/_ xwrecs ( R , A , F )
Theorem	wrecseq1 7410	Equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
|- ( R = S -> wrecs ( R , A , F ) = wrecs ( S , A , F ) )
Theorem	wrecseq2 7411	Equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
|- ( A = B -> wrecs ( R , A , F ) = wrecs ( R , B , F ) )
Theorem	wrecseq3 7412	Equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
|- ( F = G -> wrecs ( R , A , F ) = wrecs ( R , A , G ) )
Theorem	wfr3g 7413*	Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. (Contributed by Scott Fenton, 11-Feb-2011.)
|- ( ( ( R We A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( H ` ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( H ` ( G |` Pred ( R , A , y ) ) ) ) ) -> F = G )
Theorem	wfrlem1 7414*	Lemma for well-founded recursion. The final item we are interested in is the union of acceptable functions B. This lemma just changes bound variables for later use. (Contributed by Scott Fenton, 21-Apr-2011.)
|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- B = { g | E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( F ` ( g |` Pred ( R , A , w ) ) ) ) }
Theorem	wfrlem2 7415*	Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Scott Fenton, 21-Apr-2011.)
|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( g e. B -> Fun g )
Theorem	wfrlem3 7416*	Lemma for well-founded recursion. An acceptable function's domain is a subset of A. (Contributed by Scott Fenton, 21-Apr-2011.)
|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( g e. B -> dom g C_ A )
Theorem	wfrlem3a 7417*	Lemma for well-founded recursion. Show membership in the class of acceptable functions. (Contributed by Scott Fenton, 31-Jul-2020.)
|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- G e. _V   =>    |- ( G e. B <-> E. z ( G Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( G ` w ) = ( F ` ( G |` Pred ( R , A , w ) ) ) ) )
Theorem	wfrlem4 7418*	Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another one. (Contributed by Scott Fenton, 21-Apr-2011.)
|- R We A   &    |- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( ( g e. B /\ h e. B ) -> ( ( g |` ( dom g i^i dom h ) ) Fn ( dom g i^i dom h ) /\ A. a e. ( dom g i^i dom h ) ( ( g |` ( dom g i^i dom h ) ) ` a ) = ( F ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )
Theorem	wfrlem5 7419*	Lemma for well-founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( ( g e. B /\ h e. B ) -> ( ( x g u /\ x h v ) -> u = v ) )
Theorem	wfrrel 7420	The well-founded recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.)
|- F = wrecs ( R , A , G )   =>    |- Rel F
Theorem	wfrdmss 7421	The domain of the well-founded recursion generator is a subclass of A. (Contributed by Scott Fenton, 21-Apr-2011.)
|- F = wrecs ( R , A , G )   =>    |- dom F C_ A
Theorem	wfrlem8 7422	Lemma for well-founded recursion. Compute the prececessor class for an R minimal element of ( A \ dom F ). (Contributed by Scott Fenton, 21-Apr-2011.)
|- F = wrecs ( R , A , G )   =>    |- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> Pred ( R , A , X ) = Pred ( R , dom F , X ) )
Theorem	wfrdmcl 7423	Given F = wrecs ( R , A , X ) /\ X e. dom F, then its predecessor class is a subset of dom F. (Contributed by Scott Fenton, 21-Apr-2011.)
|- F = wrecs ( R , A , G )   =>    |- ( X e. dom F -> Pred ( R , A , X ) C_ dom F )
Theorem	wfrlem10 7424*	Lemma for well-founded recursion. When z is an R minimal element of ( A \ dom F ), then its predecessor class is equal to dom F. (Contributed by Scott Fenton, 21-Apr-2011.)
|- R We A   &    |- F = wrecs ( R , A , G )   =>    |- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )
Theorem	wfrfun 7425	The well-founded function generator generates a function. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- Fun F
Theorem	wfrlem12 7426*	Lemma for well-founded recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- ( y e. dom F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
Theorem	wfrlem13 7427*	Lemma for well-founded recursion. From here through wfrlem16 7430, we aim to prove that dom F = A. We do this by supposing that there is an element z of A that is not in dom F. We then define C by extending dom F with the appropriate value at z. We then show that z cannot be an R minimal element of ( A \ dom F ), meaning that ( A \ dom F ) must be empty, so dom F = A. Here, we show that C is a function extending the domain of F by one. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )
Theorem	wfrlem14 7428*	Lemma for well-founded recursion. Compute the value of C. (Contributed by Scott Fenton, 21-Apr-2011.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- ( z e. ( A \ dom F ) -> ( y e. ( dom F u. { z } ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
Theorem	wfrlem15 7429*	Lemma for well-founded recursion. When z is R minimal, C is an acceptable function. This step is where the Axiom of Replacement becomes required. (Contributed by Scott Fenton, 21-Apr-2011.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } )
Theorem	wfrlem16 7430*	Lemma for well-founded recursion. If z is R minimal in ( A \ dom F ), then C is acceptable and thus a subset of F, but dom C is bigger than dom F. Thus, z cannot be minimal, so ( A \ dom F ) must be empty, and (due to wfrdmss 7421), dom F = A. (Contributed by Scott Fenton, 21-Apr-2011.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- dom F = A
Theorem	wfrlem17 7431	Without using ax-rep 4771, show that all restrictions of wrecs are sets. (Contributed by Scott Fenton, 31-Jul-2020.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- ( X e. dom F -> ( F |` Pred ( R , A , X ) ) e. _V )
Theorem	wfr2a 7432	A weak version of wfr2 7434 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- ( X e. dom F -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )
Theorem	wfr1 7433	The Principle of Well-Founded Recursion, part 1 of 3. We start with an arbitrary function G. Then, using a base class A and a well-ordering R of A, we define a function F. This function is said to be defined by "well-founded recursion." The purpose of these three theorems is to demonstrate the properties of F. We begin by showing that F is a function over A. (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- F Fn A
Theorem	wfr2 7434	The Principle of Well-Founded Recursion, part 2 of 3. Next, we show that the value of F at any X e. A is G recursively applied to all "previous" values of F. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- ( X e. A -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )
Theorem	wfr3 7435*	The principle of Well-Founded Recursion, part 3 of 3. Finally, we show that F is unique. We do this by showing that any function H with the same properties we proved of F in wfr1 7433 and wfr2 7434 is identical to F. (Contributed by Scott Fenton, 18-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   &    |- F = wrecs ( R , A , G )   =>    |- ( ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) -> F = H )
2.4.14  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 7436*	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	iinon 7437*	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 7438*	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 7439*	A variant of onfununi 7438 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 7440*	A variant of onovuni 7439 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 7441*	There are no length om decreasing sequences in the ordinals. See also noinfep 8557 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 7442	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 7443*	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 7444*	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 7445*	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 7446*	Alternate 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 7447	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )
Theorem	smodm 7448	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( Smo A -> Ord dom A )
Theorem	smores 7449	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 7450	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 7451	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 7452	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 7453	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 7454	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 7455	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 7456	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 7457	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 7458*	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 7459	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 7460	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 7461	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 7462	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 7463	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 7464	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 7465	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 7466	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.15  "Strong" transfinite recursion
Syntax	crecs 7467	Notation for a function defined by strong transfinite recursion.
class recs ( F )
Definition	df-recs 7468	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 7506 for more details on why this definition is desirable. Unlike df-rdg 7506 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 7499 and recsval 7500 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Scott Fenton, 3-Aug-2020.)
|- recs ( F ) = wrecs ( _E , On , F )
Theorem	dfrecs3 7469*	The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.)
|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Theorem	recseq 7470	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( F = G -> recs ( F ) = recs ( G ) )
Theorem	nfrecs 7471	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F/_ x F   =>    |- F/_ xrecs ( F )
Theorem	tfrlem1 7472*	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 7473*	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 7474*	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 7475*	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 7476*	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 7477*	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 7478*	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 7479*	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 7480*	Lemma for transfinite recursion. The domain of recs is an 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 7481*	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 7482*	Lemma for transfinite recursion. Without using ax-rep 4771, 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 7483*	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 7487, 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 7484*	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 7485*	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 7486*	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 7487*	Lemma for transfinite recursion. Assuming ax-rep 4771, 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 7488*	Lemma for transfinite recursion. Without assuming ax-rep 4771, 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 7489*	Lemma for finite recursion. Without assuming ax-rep 4771, 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 7490	A weak version of tfr1 7493 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 7491	A weak version of tfr2 7494 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 7492	Without assuming ax-rep 4771, 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 7493	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 7494	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 7495*	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	tfr1ALT 7496	Alternate proof of tfr1 7493 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F = recs ( G )   =>    |- F Fn On
Theorem	tfr2ALT 7497	Alternate proof of tfr2 7494 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F = recs ( G )   =>    |- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfr3ALT 7498*	Alternate proof of tfr3 7495 using well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F = recs ( G )   =>    |- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )
Theorem	recsfnon 7499	Strong transfinite recursion defines a function on ordinals. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- recs ( F ) Fn On
Theorem	recsval 7500	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 ) ) )