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	brovmpt2ex 7001*	A binary relation of the value of an operation given by the "maps to" notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.)
|- O = ( x e. _V , y e. _V |-> { <. z , w >. | ph } )   =>    |- ( F ( V O E ) P -> ( ( V e. _V /\ E e. _V ) /\ ( F e. _V /\ P e. _V ) ) )
Theorem	sprmpt2d 7002*	The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 20-Jun-2019.)
|- M = ( v e. _V , e e. _V |-> { <. x , y >. | ( x ( v R e ) y /\ ch ) } )   &    |- ( ( ph /\ v = V /\ e = E ) -> ( ch <-> ps ) )   &    |- ( ph -> ( V e. _V /\ E e. _V ) )   &    |- ( ph -> A. x A. y ( x ( V R E ) y -> th ) )   &    |- ( ph -> { <. x , y >. | th } e. _V )   =>    |- ( ph -> ( V M E ) = { <. x , y >. | ( x ( V R E ) y /\ ps ) } )
2.4.10  Function transposition
Syntax	ctpos 7003	The transposition of a function.
class tpos F
Definition	df-tpos 7004*	Define the transposition of a function, which is a function G = tpos F satisfying G ( x , y ) = F ( y , x ). (Contributed by Mario Carneiro, 10-Sep-2015.)
|- tpos F = ( F o. ( x e. ( `' dom F u. { (/) } ) |-> U. `' { x } ) )
Theorem	tposss 7005	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F C_ G -> tpos F C_ tpos G )
Theorem	tposeq 7006	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F = G -> tpos F = tpos G )
Theorem	tposeqd 7007	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> F = G )   =>    |- ( ph -> tpos F = tpos G )
Theorem	tposssxp 7008	The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
Theorem	reltpos 7009	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- Rel tpos F
Theorem	brtpos2 7010	Value of the transposition at a pair <. A , B >.. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( B e. V -> ( Atpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )
Theorem	brtpos0 7011	The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows us to eliminate sethood hypotheses on A , B in brtpos 7013. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( A e. V -> ( (/)tpos F A <-> (/) F A ) )
Theorem	reldmtpos 7012	Necessary and sufficient condition for dom tpos F to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom tpos F <-> -. (/) e. dom F )
Theorem	brtpos 7013	The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( C e. V -> ( <. A , B >.tpos F C <-> <. B , A >. F C ) )
Theorem	ottpos 7014	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( C e. V -> ( <. A , B , C >. e. tpos F <-> <. B , A , C >. e. F ) )
Theorem	relbrtpos 7015	The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015.)
|- ( Rel F -> ( <. A , B >.tpos F C <-> <. B , A >. F C ) )
Theorem	dmtpos 7016	The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> dom tpos F = `' dom F )
Theorem	rntpos 7017	The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> ran tpos F = ran F )
Theorem	tposexg 7018	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F e. V -> tpos F e. _V )
Theorem	ovtpos 7019	The transposition swaps the arguments in a two-argument function. When F is a matrix, which is to say a function from ( 1 ... m ) X. ( 1 ... n ) to RR or some ring, tpos F is the transposition of F, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Atpos F B ) = ( B F A )
Theorem	tposfun 7020	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Fun F -> Fun tpos F )
Theorem	dftpos2 7021*	Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )
Theorem	dftpos3 7022*	Alternate definition of tpos when F has relational domain. Compare df-cnv 4864. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = { <. <. x , y >. , z >. | <. y , x >. F z } )
Theorem	dftpos4 7023*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
Theorem	tpostpos 7024	Value of the double transposition for a general class F. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- tpos tpos F = ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
Theorem	tpostpos2 7025	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- ( ( Rel F /\ Rel dom F ) -> tpos tpos F = F )
Theorem	tposfn2 7026	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F Fn A -> tpos F Fn `' A ) )
Theorem	tposfo2 7027	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -onto-> B -> tpos F : `' A -onto-> B ) )
Theorem	tposf2 7028	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A --> B -> tpos F : `' A --> B ) )
Theorem	tposf12 7029	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -1-1-> B -> tpos F : `' A -1-1-> B ) )
Theorem	tposf1o2 7030	Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -1-1-onto-> B -> tpos F : `' A -1-1-onto-> B ) )
Theorem	tposfo 7031	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( F : ( A X. B ) -onto-> C -> tpos F : ( B X. A ) -onto-> C )
Theorem	tposf 7032	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( F : ( A X. B ) --> C -> tpos F : ( B X. A ) --> C )
Theorem	tposfn 7033	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( F Fn ( A X. B ) -> tpos F Fn ( B X. A ) )
Theorem	tpos0 7034	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
|- tpos (/) = (/)
Theorem	tposco 7035	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- tpos ( F o. G ) = ( F o. tpos G )
Theorem	tpossym 7036*	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 7037	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = G   =>    |- tpos F = tpos G
Theorem	tposex 7038	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F e. _V   =>    |- tpos F e. _V
Theorem	nftpos 7039	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F/_ x F   =>    |- F/_ xtpos F
Theorem	tposoprab 7040*	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 7041*	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 7042	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 7043	Extend class notation to include the currying function.
class curry A
Syntax	cunc 7044	Extend class notation to include the uncurrying function.
class uncurry A
Definition	df-cur 7045*	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 7046*	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 7047*	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 7048*	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 7049*	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 7050	Extend class notation with undefined value function.
class Undef
Definition	df-undef 7051	Define the undefined value function, whose value at set s is guaranteed not to be a member of s (see pwuninel 7053). (Contributed by NM, 15-Sep-2011.)
|- Undef = ( s e. _V |-> ~P U. s )
Theorem	pwuninel2 7052	Direct proof of pwuninel 7053 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 7053	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 7052. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
|- -. ~P U. A e. A
Theorem	undefval 7054	Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 7056 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( S e. V -> ( Undef ` S ) = ~P U. S )
Theorem	undefnel2 7055	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 7056	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 7057	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 7058	Declare syntax for the well-founded recursive function generator.
class wrecs ( R , A , F )
Definition	df-wrecs 7059*	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 7085, wfr2 7086, and wfr3 7087. (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 7060	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 7061	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 7062	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 7063	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 7064	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 7065*	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 7066*	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 7067*	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 7068*	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 7069*	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 7070*	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 7071*	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 7072	The well-founded recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.)
|- F = wrecs ( R , A , G )   =>    |- Rel F
Theorem	wfrdmss 7073	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 7074	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 7075	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 7076*	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 7077	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 7078*	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 7079*	Lemma for well-founded recursion. From here through wfrlem16 7082, 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 7080*	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 7081*	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 7082*	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 7073), 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 7083	Without using ax-rep 4531, 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 7084	A weak version of wfr2 7086 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 7085	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 7086	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 7087*	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 7085 and wfr2 7086 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 7088*	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 7089*	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 7090*	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 7091*	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 7092*	A variant of onfununi 7091 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 7093*	A variant of onovuni 7092 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 7094*	There are no length om decreasing sequences in the ordinals. See also noinfep 8196 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 7095	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 7096*	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 7097*	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 7098*	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 7099*	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 7100	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )