P. 255 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	setlikespec 25401	If R is set-like in A, then all predecessors classes of elements of A exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
Theorem	predidm 25402	Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.)
|- Pred ( R , Pred ( R , A , X ) , X ) = Pred ( R , A , X )
Theorem	predin 25403	Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
|- Pred ( R , ( A i^i B ) , X ) = ( Pred ( R , A , X ) i^i Pred ( R , B , X ) )
Theorem	predun 25404	Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.)
|- Pred ( R , ( A u. B ) , X ) = ( Pred ( R , A , X ) u. Pred ( R , B , X ) )
Theorem	preddif 25405	Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.)
|- Pred ( R , ( A \ B ) , X ) = ( Pred ( R , A , X ) \ Pred ( R , B , X ) )
Theorem	predep 25406	The predecessor under the epsilon relationship is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
|- ( X e. B -> Pred ( _E , A , X ) = ( A i^i X ) )
Theorem	predon 25407	For an ordinal, the predecessor under _E and On is an identity relationship. (Contributed by Scott Fenton, 27-Mar-2011.)
|- ( A e. On -> Pred ( _E , On , A ) = A )
Theorem	epsetlike 25408	The epsilon relationship is set-like. (Contributed by Scott Fenton, 27-Mar-2011.)
|- A. x e. A Pred ( _E , A , x ) e. _V
Theorem	setlikess 25409*	If R is set-like over A, then it is set-like over any subclass of A. (Contributed by Scott Fenton, 28-Mar-2011.)
|- ( ( A C_ B /\ A. x e. B Pred ( R , B , x ) e. _V ) -> A. x e. A Pred ( R , A , x ) e. _V )
Theorem	preddowncl 25410*	A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.)
|- ( ( B C_ A /\ A. x e. B Pred ( R , A , x ) C_ B ) -> ( X e. B -> Pred ( R , B , X ) = Pred ( R , A , X ) ) )
Theorem	predpoirr 25411	Given a partial ordering, X is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.)
|- ( R Po A -> -. X e. Pred ( R , A , X ) )
Theorem	predfrirr 25412	Given a well-founded relationship, X is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.)
|- ( R Fr A -> -. X e. Pred ( R , A , X ) )
Theorem	pred0 25413	The predecessor class over (/) is always (/) (Contributed by Scott Fenton, 16-Apr-2011.)
|- Pred ( R , (/) , X ) = (/)
Theorem	preduz 25414	The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014.)
|- ( N e. ( ZZ>= ` M ) -> Pred ( < , ( ZZ>= ` M ) , N ) = ( M ... ( N - 1 ) ) )
Theorem	prednn 25415	The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013.)
|- ( N e. NN -> Pred ( < , NN , N ) = ( 1 ... ( N - 1 ) ) )
Theorem	prednn0 25416	The value of the predecessor class over NN0. (Contributed by Scott Fenton, 9-May-2014.)
|- ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
Theorem	predfz 25417	Calculate the predecessor of an integer under a finite set of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Proof shortened by Mario Carneiro, 3-May-2015.)
|- ( K e. ( M ... N ) -> Pred ( < , ( M ... N ) , K ) = ( M ... ( K - 1 ) ) )
19.7.21  (Trans)finite Recursion Theorems
Theorem	tfisg 25418*	A closed form of tfis 4793. (Contributed by Scott Fenton, 8-Jun-2011.)
|- ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> A. x e. On ph )
19.7.22  Well-founded induction
Theorem	tz6.26 25419*	All nonempty (possibly proper) subclasses of A, which has a well-founded relation R, have R-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )
Theorem	tz6.26i 25420*	All nonempty (possibly proper) subclasses of A, which has a well-founded relation R, have R-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   =>    |- ( ( B C_ A /\ B =/= (/) ) -> E. y e. B Pred ( R , B , y ) = (/) )
Theorem	wfi 25421*	The Principle of Well-Founded Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if B is a subclass of a well-ordered class A with the property that every element of B whose inital segment is included in A is itself equal to A. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B )
Theorem	wfii 25422*	The Principle of Well-Founded Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if B is a subclass of a well-ordered class A with the property that every element of B whose inital segment is included in A is itself equal to A. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R We A   &    |- R Se A   =>    |- ( ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) -> A = B )
Theorem	wfisg 25423*	Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A. (Contributed by Scott Fenton, 11-Feb-2011.)
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )   =>    |- ( ( R We A /\ R Se A ) -> A. y e. A ph )
Theorem	wfis 25424*	Well-Founded Induction Schema. If all elements less than a given set x of the well-founded class A have a property (induction hypothesis), then all elements of A have that property. (Contributed by Scott Fenton, 29-Jan-2011.)
|- R We A   &    |- R Se A   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	wfis2fg 25425*	Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.)
|- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( ( R We A /\ R Se A ) -> A. y e. A ph )
Theorem	wfis2f 25426*	Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
|- R We A   &    |- R Se A   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	wfis2g 25427*	Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.)
|- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( ( R We A /\ R Se A ) -> A. y e. A ph )
Theorem	wfis2 25428*	Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
|- R We A   &    |- R Se A   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	wfis3 25429*	Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.)
|- R We A   &    |- R Se A   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y = B -> ( ph <-> ch ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( B e. A -> ch )
Theorem	uzsinds 25430*	Strong (or "total") induction principle over a set of upper integers. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. ( ZZ>= ` M ) -> ( A. y e. ( M ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ch )
Theorem	nnsinds 25431*	Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. NN -> ( A. y e. ( 1 ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. NN -> ch )
Theorem	nn0sinds 25432*	Strong (or "total") induction principle over the non-negative integers. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. NN0 -> ( A. y e. ( 0 ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. NN0 -> ch )
Theorem	omsinds 25433*	Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = A -> ( ph <-> ch ) )   &    |- ( x e. om -> ( A. y e. x ps -> ph ) )   =>    |- ( A e. om -> ch )
19.7.23  Transitive closure under a relationship
Syntax	ctrpred 25434	Define the transitive predecessor class as a class.
class TrPred ( R , A , X )
Definition	df-trpred 25435*	Define the transitive predecessors of a class X under a relationship R and a class A. This class can be thought of as the "smallest" class containing all elements of A that are linked to X by a chain of R relationships (see trpredtr 25447 and trpredmintr 25448). Definition based off of Lemma 4.2 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory (check The Internet Archive for it now as Prof. Monk appears to have rewritten his website). (Contributed by Scott Fenton, 2-Feb-2011.)
|- TrPred ( R , A , X ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om )
Theorem	dftrpred2 25436*	A definition of the transitive predecessors of a class in terms of indexed union. (Contributed by Scott Fenton, 28-Apr-2012.)
|- TrPred ( R , A , X ) = U_ i e. om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om ) ` i )
Theorem	trpredeq1 25437	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( R = S -> TrPred ( R , A , X ) = TrPred ( S , A , X ) )
Theorem	trpredeq2 25438	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A = B -> TrPred ( R , A , X ) = TrPred ( R , B , X ) )
Theorem	trpredeq3 25439	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( X = Y -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) )
Theorem	trpredeq1d 25440	Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( ph -> R = S )   =>    |- ( ph -> TrPred ( R , A , X ) = TrPred ( S , A , X ) )
Theorem	trpredeq2d 25441	Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> TrPred ( R , A , X ) = TrPred ( R , B , X ) )
Theorem	trpredeq3d 25442	Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( ph -> X = Y )   =>    |- ( ph -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) )
Theorem	eltrpred 25443*	A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not really meant to be used directly: instead refer to trpredpred 25445 and trpredmintr 25448. (Contributed by Scott Fenton, 28-Apr-2012.)
|- ( Y e. TrPred ( R , A , X ) <-> E. i e. om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om ) ` i ) )
Theorem	trpredlem1 25444*	Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subsets of the base set. (Contributed by Scott Fenton, 28-Apr-2012.)
|- ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` om ) ` i ) C_ A )
Theorem	trpredpred 25445	Assuming it exists, the predecessor class is a subset of the transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011.)
|- ( Pred ( R , A , X ) e. B -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
Theorem	trpredss 25446	The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011.)
|- ( Pred ( R , A , X ) e. B -> TrPred ( R , A , X ) C_ A )
Theorem	trpredtr 25447	The transitive predecessors are transitive in R and A (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )
Theorem	trpredmintr 25448*	The transitive predecessors form the smallest class transitive in R and A. That is, if B is another R, A transitive class containing Pred ( R , A , X ), then TrPred ( R , A , X ) C_ B (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> TrPred ( R , A , X ) C_ B )
Theorem	trpredelss 25449	Given a transitive predecessor Y of X, the transitive predecessors of Y are a subset of the transitive predecessors of X. (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )
Theorem	dftrpred3g 25450*	The transitive predecessors of X are equal to the predecessors of X together with their transitive predecessors. (Contributed by Scott Fenton, 26-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
Theorem	dftrpred4g 25451*	Another recursive expression for the transitive predecessors. (Contributed by Scott Fenton, 27-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = U_ y e. Pred ( R , A , X ) ( { y } u. TrPred ( R , A , y ) ) )
Theorem	trpredpo 25452	If R partially orders A, then the transitive predecessors are the same as the immediate predecessors . (Contributed by Scott Fenton, 28-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( R Po A /\ X e. A /\ R Se A ) -> TrPred ( R , A , X ) = Pred ( R , A , X ) )
Theorem	trpred0 25453	The class of transitive predecessors is empty when A is empty. (Contributed by Scott Fenton, 30-Apr-2012.)
|- TrPred ( R , (/) , X ) = (/)
Theorem	trpredex 25454	The transitive predecessors of a relation form a set (NOTE: this is the first theorem in the transitive predecessor series that requires infinity). (Contributed by Scott Fenton, 18-Feb-2011.)
|- TrPred ( R , A , X ) e. _V
Theorem	trpredrec 25455*	If Y is an R, A transitive predecessor, then it is either an immediate predecessor or there is a transitive predecessor between Y and X (Contributed by Scott Fenton, 9-May-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) )
19.7.24  Founded Induction
Theorem	frmin 25456*	Every (possibly proper) subclass of a class A with a founded, set-like relation R has a minimal element. Lemma 4.3 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory. This is a very strong generalization of tz6.26 25419 and tz7.5 4562. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )
Theorem	frind 25457*	The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 25456). This principle states that if B is a subclass of a founded class A with the property that every element of B whose initial segment is included in A is itself equal to A. Compare wfi 25421 and tfi 4792, which are special cases of this theorem that do not require the axiom of infinity to prove. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( R Fr A /\ R Se A ) /\ ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) ) -> A = B )
Theorem	frindi 25458*	The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 25456). This principle states that if B is a subclass of a founded class A with the property that every element of B whose initial segment is included in A is itself equal to A. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R Fr A   &    |- R Se A   =>    |- ( ( B C_ A /\ A. y e. A ( Pred ( R , A , y ) C_ B -> y e. B ) ) -> A = B )
Theorem	frinsg 25459*	Founded Induction Schema. If a property passes from all elements less than y of a founded class A to y itself (induction hypothesis), then the property holds for all elements of A. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )   =>    |- ( ( R Fr A /\ R Se A ) -> A. y e. A ph )
Theorem	frins 25460*	Founded Induction Schema. If a property passes from all elements less than y of a founded class A to y itself (induction hypothesis), then the property holds for all elements of A. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R Fr A   &    |- R Se A   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	frins2fg 25461*	Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- ( ( R Fr A /\ R Se A ) -> A. y e. A ph )
Theorem	frins2f 25462*	Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- R Fr A   &    |- R Se A   &    |- F/ y ps   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	frins2g 25463*	Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 8-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   &    |- ( y = z -> ( ph <-> ps ) )   =>    |- ( ( R Fr A /\ R Se A ) -> A. y e. A ph )
Theorem	frins2 25464*	Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R Fr A   &    |- R Se A   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( y e. A -> ph )
Theorem	frins3 25465*	Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R Fr A   &    |- R Se A   &    |- ( y = z -> ( ph <-> ps ) )   &    |- ( y = B -> ( ph <-> ch ) )   &    |- ( y e. A -> ( A. z e. Pred ( R , A , y ) ps -> ph ) )   =>    |- ( B e. A -> ch )
19.7.25  Ordering Ordinal Sequences
Theorem	orderseqlem 25466*	Lemma for poseq 25467 and soseq 25468. The function value of a sequene is either in A or null. (Contributed by Scott Fenton, 8-Jun-2011.)
|- F = { f | E. x e. On f : x --> A }   =>    |- ( G e. F -> ( G ` X ) e. ( A u. { (/) } ) )
Theorem	poseq 25467*	A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)
|- R Po ( A u. { (/) } )   &    |- F = { f | E. x e. On f : x --> A }   &    |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) }   =>    |- S Po F
Theorem	soseq 25468*	A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)
|- R Or ( A u. { (/) } )   &    |- F = { f | E. x e. On f : x --> A }   &    |- S = { <. f , g >. | ( ( f e. F /\ g e. F ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) R ( g ` x ) ) ) }   &    |- -. (/) e. A   =>    |- S Or F
19.7.26  Well-founded recursion
Theorem	wfr3g 25469*	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 25470*	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 ) = ( G ` ( 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 ) = ( G ` ( g |` Pred ( R , A , w ) ) ) ) }
Theorem	wfrlem2 25471*	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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( g e. B -> Fun g )
Theorem	wfrlem3 25472*	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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( g e. B -> dom g C_ A )
Theorem	wfrlem4 25473*	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 ) = ( G ` ( 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 ) = ( G ` ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )
Theorem	wfrlem5 25474*	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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   =>    |- ( ( g e. B /\ h e. B ) -> ( ( x g u /\ x h v ) -> u = v ) )
Theorem	wfrlem6 25475*	Lemma for well-founded recursion. The union of all acceptable functions is a relationship. (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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- Rel F
Theorem	wfrlem7 25476*	Lemma for well-founded recursion. The domain of F is a subclass 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- dom F C_ A
Theorem	wfrlem8 25477*	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.)
|- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> Pred ( R , A , X ) = Pred ( R , dom F , X ) )
Theorem	wfrlem9 25478*	Lemma for well-founded recursion. If X e. dom F, then its predecessor class is a subset of dom F. (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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( X e. dom F -> Pred ( R , A , X ) C_ dom F )
Theorem	wfrlem10 25479*	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   &    |- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )
Theorem	wfrlem11 25480*	Lemma for well-founded recursion. The union of all acceptable functions is a function. (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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- Fun F
Theorem	wfrlem12 25481*	Lemma for well-founded recursion. Here, we compute the value of F (the union of all acceptable functions). (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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( y e. dom F -> ( F ` y ) = ( G ` ( F |` Pred ( R , A , y ) ) ) )
Theorem	wfrlem13 25482*	Lemma for well-founded recursion. From here through wfrlem16 25485, 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   &    |- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )
Theorem	wfrlem14 25483*	Lemma for well-founded recursion. Compute the value of C. (Contributed by Scott Fenton, 21-Apr-2011.)
|- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   &    |- 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 25484*	Lemma for well-founded recursion. When z is R minimal, C is an acceptable function. (Contributed by Scott Fenton, 21-Apr-2011.)
|- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C e. B )
Theorem	wfrlem16 25485*	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 wfrlem7 25476), dom F = A. (Contributed by Scott Fenton, 21-Apr-2011.)
|- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   &    |- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )   =>    |- dom F = A
Theorem	wfr1 25486*	The Principle of Well-Founded Recursion, part 1 of 3. We start with an arbitrary function G and a class of "acceptable" functions B. 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   &    |- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- F Fn A
Theorem	wfr2 25487*	The Principle of Well-Founded Recursion, part 2 of 3. Next, we show that the value of F at any z 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   &    |- 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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( z e. A -> ( F ` z ) = ( G ` ( F |` Pred ( R , A , z ) ) ) )
Theorem	wfr2c 25488*	Generalize wfr2 25487 to class arguments. (Contributed by Scott Fenton, 6-Aug-2013.) (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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( X e. A -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) )
Theorem	wfr3 25489*	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 25486 and wfr2 25487 is identical to F. (Contributed by Scott Fenton, 18-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 ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }   &    |- F = U. B   =>    |- ( ( H Fn A /\ A. z e. A ( H ` z ) = ( G ` ( H |` Pred ( R , A , z ) ) ) ) -> F = H )
19.7.27  Transfinite recursion via Well-founded recursion
Theorem	tfrALTlem 25490*	Lemma for deriving transfinite recursion from well-founded recursion. (Contributed by Scott Fenton, 22-Apr-2011.)
|- { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x ( f Fn x /\ ( x C_ On /\ A. y e. x Pred ( _E , On , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( _E , On , y ) ) ) ) }
Theorem	tfr1ALT 25491*	tfr1 6617 via well-founded recursion. (Contributed by Scott Fenton, 17-Aug-1994.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof modification is discouraged.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- F = U. A   =>    |- F Fn On
Theorem	tfr2ALT 25492*	tfr2 6618 via well-founded recursion. (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof modification is discouraged.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- F = U. A   =>    |- ( z e. On -> ( F ` z ) = ( G ` ( F |` z ) ) )
Theorem	tfr3ALT 25493*	tfr3 6619 via well-founded recursion. (Contributed by Scott Fenton, 22-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof modification is discouraged.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- F = U. A   =>    |- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )
19.7.28  Founded Recursion
Theorem	frr3g 25494*	Functions defined by founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( ( ( R Fr A /\ R Se A ) /\ ( F Fn A /\ A. y e. A ( F ` y ) = ( y H ( F |` Pred ( R , A , y ) ) ) ) /\ ( G Fn A /\ A. y e. A ( G ` y ) = ( y H ( G |` Pred ( R , A , y ) ) ) ) ) -> F = G )
Theorem	frrlem1 25495*	Lemma for 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 Paul Chapman, 21-Apr-2012.)
|- 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 ) = ( y G ( 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 ) = ( w G ( g |` Pred ( R , A , w ) ) ) ) ) }
Theorem	frrlem2 25496*	Lemma for founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.)
|- 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) ) }   =>    |- ( g e. B -> Fun g )
Theorem	frrlem3 25497*	Lemma for founded recursion. An acceptable function's domain is a subset of A. (Contributed by Paul Chapman, 21-Apr-2012.)
|- 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) ) }   =>    |- ( g e. B -> dom g C_ A )
Theorem	frrlem4 25498*	Lemma for founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.)
|- 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 ) = ( y G ( 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 ) = ( a G ( ( g |` ( dom g i^i dom h ) ) |` Pred ( R , ( dom g i^i dom h ) , a ) ) ) ) )
Theorem	frrlem5 25499*	Lemma for founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Paul Chapman, 21-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- R Fr 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) ) }   =>    |- ( ( g e. B /\ h e. B ) -> ( ( x g u /\ x h v ) -> u = v ) )
Theorem	frrlem5b 25500*	Lemma for founded recursion. The union of a subclass of B is a relationship. (Contributed by Paul Chapman, 29-Apr-2012.)
|- R Fr 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) ) }   =>    |- ( C C_ B -> Rel U. C )