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	tposfn 7001	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( F Fn ( A X. B ) -> tpos F Fn ( B X. A ) )
Theorem	tpos0 7002	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
|- tpos (/) = (/)
Theorem	tposco 7003	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- tpos ( F o. G ) = ( F o. tpos G )
Theorem	tpossym 7004*	Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( F Fn ( A X. A ) -> (tpos F = F <-> A. x e. A A. y e. A ( x F y ) = ( y F x ) ) )
Theorem	tposeqi 7005	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = G   =>    |- tpos F = tpos G
Theorem	tposex 7006	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F e. _V   =>    |- tpos F e. _V
Theorem	nftpos 7007	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F/_ x F   =>    |- F/_ xtpos F
Theorem	tposoprab 7008*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = { <. <. x , y >. , z >. | ph }   =>    |- tpos F = { <. <. y , x >. , z >. | ph }
Theorem	tposmpt2 7009*	Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- tpos F = ( y e. B , x e. A |-> C )
Theorem	tposconst 7010	The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018.)
|- tpos ( ( A X. B ) X. { C } ) = ( ( B X. A ) X. { C } )
2.4.11  Curry and uncurry
Syntax	ccur 7011	Extend class notation to include the currying function.
class curry A
Syntax	cunc 7012	Extend class notation to include the uncurrying function.
class uncurry A
Definition	df-cur 7013*	Define the currying of F, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- curry F = ( x e. dom dom F |-> { <. y , z >. | <. x , y >. F z } )
Definition	df-unc 7014*	Define the uncurrying of F, which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- uncurry F = { <. <. x , y >. , z >. | y ( F ` x ) z }
Theorem	mpt2curryd 7015*	The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019.)
|- F = ( x e. X , y e. Y |-> C )   &    |- ( ph -> A. x e. X A. y e. Y C e. V )   &    |- ( ph -> Y =/= (/) )   =>    |- ( ph -> curry F = ( x e. X |-> ( y e. Y |-> C ) ) )
Theorem	mpt2curryvald 7016*	The value of a curried operation given in maps-to notation is a function over the second argument of the original operation. (Contributed by AV, 27-Oct-2019.)
|- F = ( x e. X , y e. Y |-> C )   &    |- ( ph -> A. x e. X A. y e. Y C e. V )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A e. X )   =>    |- ( ph -> (curry F ` A ) = ( y e. Y |-> [_ A / x ]_ C ) )
Theorem	fvmpt2curryd 7017*	The value of the value of a curried operation given in maps-to notation is the operation value of the original operation. (Contributed by AV, 27-Oct-2019.)
|- F = ( x e. X , y e. Y |-> C )   &    |- ( ph -> A. x e. X A. y e. Y C e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   =>    |- ( ph -> ( (curry F ` A ) ` B ) = ( A F B ) )
2.4.12  Undefined values
Syntax	cund 7018	Extend class notation with undefined value function.
class Undef
Definition	df-undef 7019	Define the undefined value function, whose value at set s is guaranteed not to be a member of s (see pwuninel 7021). (Contributed by NM, 15-Sep-2011.)
|- Undef = ( s e. _V |-> ~P U. s )
Theorem	pwuninel2 7020	Direct proof of pwuninel 7021 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 7021	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 7020. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- -. ~P U. A e. A
Theorem	undefval 7022	Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 7024 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( S e. V -> ( Undef ` S ) = ~P U. S )
Theorem	undefnel2 7023	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 7024	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 7025	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 7026	Declare syntax for the well-founded recursive function generator.
class wrecs ( R , A , F )
Definition	df-wrecs 7027*	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 7053, wfr2 7054, and wfr3 7055. (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 7028	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 7029	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 7030	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 7031	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 7032	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 7033*	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 7034*	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 7035*	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 7036*	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 7037*	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 7038*	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 7039*	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 7040	The well-founded recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.)
|- F = wrecs ( R , A , G )   =>    |- Rel F
Theorem	wfrdmss 7041	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 7042	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 7043	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 7044*	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 7045	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 7046*	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 7047*	Lemma for well-founded recursion. From here through wfrlem16 7050, 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 7048*	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 7049*	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 7050*	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 7041), 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 7051	Without using ax-rep 4529, 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 7052	A weak version of wfr2 7054 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 7053	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 7054	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 7055*	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 7053 and wfr2 7054 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 7056*	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 7057*	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 7058*	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 7059*	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 7060*	A variant of onfununi 7059 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 7061*	A variant of onovuni 7060 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 7062*	There are no length om decreasing sequences in the ordinals. See also noinfep 8155 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 7063	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 7064*	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 7065*	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 7066*	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 7067*	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 7068	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )
Theorem	smodm 7069	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( Smo A -> Ord dom A )
Theorem	smores 7070	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 7071	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 7072	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 7073	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 7074	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 7075	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 7076	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 7077	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 7078	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 7079*	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 7080	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 7081	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 7082	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 7083	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 7084	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 7085	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 7086	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 7087	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 7088	Notation for a function defined by strong transfinite recursion.
class recs ( F )
Definition	df-recs 7089	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 7127 for more details on why this definition is desirable. Unlike df-rdg 7127 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 7120 and recsval 7121 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 7090*	The old definition of transfinite recursion. This version is preferred for developement, 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 7091	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( F = G -> recs ( F ) = recs ( G ) )
Theorem	nfrecs 7092	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F/_ x F   =>    |- F/_ xrecs ( F )
Theorem	tfrlem1 7093*	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 7094*	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 7095*	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 7096*	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 7097*	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 7098*	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 7099*	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 7100*	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 )