P. 318 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31701-31800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfrdg2 31701*	Alternate definition of the recursive function generator when I is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( I e. V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
Theorem	dfrdg3 31702*	Generalization of dfrdg2 31701 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
20.8.13  Defined equality axioms
Theorem	axextdfeq 31703	A version of ax-ext 2602 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
|- E. z ( ( z e. x -> z e. y ) -> ( ( z e. y -> z e. x ) -> ( x e. w -> y e. w ) ) )
Theorem	ax8dfeq 31704	A version of ax-8 1992 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.)
|- E. z ( ( z e. x -> z e. y ) -> ( w e. x -> w e. y ) )
Theorem	axextdist 31705	ax-ext 2602 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. z ( z e. x <-> z e. y ) -> x = y ) )
Theorem	axext4dist 31706	axext4 2606 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( x = y <-> A. z ( z e. x <-> z e. y ) ) )
Theorem	19.12b 31707*	Version of 19.12vv 2180 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )
Theorem	exnel 31708	There is always a set not in y. (Contributed by Scott Fenton, 13-Dec-2010.)
|- E. x -. x e. y
Theorem	distel 31709	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 4847 and elirrv 8504.) (Contributed by Scott Fenton, 15-Dec-2010.)
|- ( -. A. y y = x <-> -. A. y -. x e. y )
Theorem	axextndbi 31710	axextnd 9413 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.)
|- E. z ( x = y <-> ( z e. x <-> z e. y ) )
20.8.14  Hypothesis builders
Theorem	hbntg 31711	A more general form of hbnt 2144. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( A. x ( ph -> A. x ps ) -> ( -. ps -> A. x -. ph ) )
Theorem	hbimtg 31712	A more general and closed form of hbim 2127. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( ( A. x ( ph -> A. x ch ) /\ ( ps -> A. x th ) ) -> ( ( ch -> ps ) -> A. x ( ph -> th ) ) )
Theorem	hbaltg 31713	A more general and closed form of hbal 2036. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( A. x ( ph -> A. y ps ) -> ( A. x ph -> A. y A. x ps ) )
Theorem	hbng 31714	A more general form of hbn 2146. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( ph -> A. x ps )   =>    |- ( -. ps -> A. x -. ph )
Theorem	hbimg 31715	A more general form of hbim 2127. (Contributed by Scott Fenton, 13-Dec-2010.)
|- ( ph -> A. x ps )   &    |- ( ch -> A. x th )   =>    |- ( ( ps -> ch ) -> A. x ( ph -> th ) )
20.8.15  (Trans)finite Recursion Theorems
Theorem	tfisg 31716*	A closed form of tfis 7054. (Contributed by Scott Fenton, 8-Jun-2011.)
|- ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> A. x e. On ph )
20.8.16  Transitive closure under a relationship
Syntax	ctrpred 31717	Define the transitive predecessor class as a class.
class TrPred ( R , A , X )
Definition	df-trpred 31718*	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 31730 and trpredmintr 31731). 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 31719*	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 31720	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( R = S -> TrPred ( R , A , X ) = TrPred ( S , A , X ) )
Theorem	trpredeq2 31721	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( A = B -> TrPred ( R , A , X ) = TrPred ( R , B , X ) )
Theorem	trpredeq3 31722	Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.)
|- ( X = Y -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) )
Theorem	trpredeq1d 31723	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 31724	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 31725	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 31726*	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 31728 and trpredmintr 31731. (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 31727*	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 31728	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 31729	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 31730	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 31731*	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 31732	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 31733*	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 31734*	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 31735	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 31736	The class of transitive predecessors is empty when A is empty. (Contributed by Scott Fenton, 30-Apr-2012.)
|- TrPred ( R , (/) , X ) = (/)
Theorem	trpredex 31737	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 31738*	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 ) ) )
20.8.17  Founded Induction
Theorem	frmin 31739*	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 5711 and tz7.5 5744. (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 31740*	The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 31739). 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 5713 and tfi 7053, 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 31741*	The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 31739). 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 31742*	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 31743*	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 31744*	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 31745*	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 31746*	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 31747*	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 31748*	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 )
20.8.18  Ordering Ordinal Sequences
Theorem	orderseqlem 31749*	Lemma for poseq 31750 and soseq 31751. 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 31750*	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 31751*	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
20.8.19  Well-founded zero, successor, and limits
Syntax	cwsuc 31752	Declare the syntax for well-founded successor.
class wsuc ( R , A , X )
Syntax	cwsucOLD 31753	Declare the syntax for well-founded successor. (New usage is discouraged.)
class wsucOLD ( R , A , X )
Syntax	cwlim 31754	Declare the syntax for well-founded limit class.
class WLim ( R , A )
Syntax	cwlimOLD 31755	Declare the syntax for well-founded limit class. (New usage is discouraged.)
class WLimOLD ( R , A )
Definition	df-wsuc 31756	Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
|- wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
Definition	df-wsucOLD 31757	Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) Obsolete version of df-wsuc 31756 as of 10-Oct-2021. (New usage is discouraged.)
|- wsucOLD ( R , A , X ) = sup ( Pred ( `' R , A , X ) , A , `' R )
Definition	df-wlim 31758*	Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
|- WLim ( R , A ) = { x e. A | ( x =/= inf ( A , A , R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
Definition	df-wlimOLD 31759*	Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of df-wlim 31758 as of 10-Oct-2021. (New usage is discouraged.)
|- WLimOLD ( R , A ) = { x e. A | ( x =/= sup ( A , A , `' R ) /\ x = sup ( Pred ( R , A , x ) , A , R ) ) }
Theorem	wsuceq123 31760	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- ( ( R = S /\ A = B /\ X = Y ) -> wsuc ( R , A , X ) = wsuc ( S , B , Y ) )
Theorem	wsuceq1 31761	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( R = S -> wsuc ( R , A , X ) = wsuc ( S , A , X ) )
Theorem	wsuceq2 31762	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( A = B -> wsuc ( R , A , X ) = wsuc ( R , B , X ) )
Theorem	wsuceq3 31763	Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
|- ( X = Y -> wsuc ( R , A , X ) = wsuc ( R , A , Y ) )
Theorem	nfwsuc 31764	Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- F/_ x R   &    |- F/_ x A   &    |- F/_ x X   =>    |- F/_ xwsuc ( R , A , X )
Theorem	wlimeq12 31765	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- ( ( R = S /\ A = B ) -> WLim ( R , A ) = WLim ( S , B ) )
Theorem	wlimeq1 31766	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
|- ( R = S -> WLim ( R , A ) = WLim ( S , A ) )
Theorem	wlimeq2 31767	Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
|- ( A = B -> WLim ( R , A ) = WLim ( R , B ) )
Theorem	nfwlim 31768	Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/_ xWLim ( R , A )
Theorem	elwlim 31769	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
|- ( X e. WLim ( R , A ) <-> ( X e. A /\ X =/= inf ( A , A , R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) )
Theorem	elwlimOLD 31770	Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) Obsolete version of elwlim 31769 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( X e. WLimOLD ( R , A ) <-> ( X e. A /\ X =/= sup ( A , A , `' R ) /\ X = sup ( Pred ( R , A , X ) , A , R ) ) )
Theorem	wzel 31771	The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
|- ( ( R We A /\ R Se A /\ A =/= (/) ) -> inf ( A , A , R ) e. A )
Theorem	wzelOLD 31772	The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) Obsolete version of wzel 31771 as of 10-Oct-2021. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( R We A /\ R Se A /\ A =/= (/) ) -> sup ( A , A , `' R ) e. A )
Theorem	wsuclem 31773*	Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.)
|- ( ph -> R We A )   &    |- ( ph -> R Se A )   &    |- ( ph -> X e. V )   &    |- ( ph -> E. w e. A X R w )   =>    |- ( ph -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. y R x /\ A. y e. A ( x R y -> E. z e. Pred ( `' R , A , X ) z R y ) ) )
Theorem	wsuclemOLD 31774*	Obsolete version of wsuclem 31773 as of 10-Oct-2021. (Contributed by Scott Fenton, 15-Jun-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> R We A )   &    |- ( ph -> R Se A )   &    |- ( ph -> X e. V )   &    |- ( ph -> E. w e. A X R w )   =>    |- ( ph -> E. x e. A ( A. y e. Pred ( `' R , A , X ) -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. Pred ( `' R , A , X ) y `' R z ) ) )
Theorem	wsucex 31775	Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- ( ph -> R Or A )   =>    |- ( ph -> wsuc ( R , A , X ) e. _V )
Theorem	wsuccl 31776*	If X is a set with an R successor in A, then its well-founded successor is a member of A. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- ( ph -> R We A )   &    |- ( ph -> R Se A )   &    |- ( ph -> X e. V )   &    |- ( ph -> E. y e. A X R y )   =>    |- ( ph -> wsuc ( R , A , X ) e. A )
Theorem	wsuclb 31777	A well-founded successor is a lower bound on points after X. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
|- ( ph -> R We A )   &    |- ( ph -> R Se A )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. A )   &    |- ( ph -> X R Y )   =>    |- ( ph -> -. Y Rwsuc ( R , A , X ) )
Theorem	wlimss 31778	The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
|- WLim ( R , A ) C_ A
20.8.20  Founded Recursion
Theorem	frr3g 31779*	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 31780*	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 31781*	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 31782*	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 31783*	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 31784*	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 31785*	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 )
Theorem	frrlem5c 31786*	Lemma for founded recursion. The union of a subclass of B is a function. (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 -> Fun U. C )
Theorem	frrlem5d 31787*	Lemma for founded recursion. The domain of the union of a subset of B is a subset of A. (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 -> dom U. C C_ A )
Theorem	frrlem5e 31788*	Lemma for founded recursion. The domain of the union of a subset of B is closed under predecessors. (Contributed by Paul Chapman, 1-May-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 -> ( X e. dom U. C -> Pred ( R , A , X ) C_ dom U. C ) )
Theorem	frrlem6 31789*	Lemma for founded recursion. The union of all acceptable functions is a relationship. (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 ) ) ) ) ) }   &    |- F = U. B   =>    |- Rel F
Theorem	frrlem7 31790*	Lemma for founded recursion. The domain of F is a subclass 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 ) ) ) ) ) }   &    |- F = U. B   =>    |- dom F C_ A
Theorem	frrlem10 31791*	Lemma for founded recursion. The union of all acceptable functions is a function. (Contributed by Paul Chapman, 21-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 ) ) ) ) ) }   &    |- F = U. B   =>    |- Fun F
Theorem	frrlem11 31792*	Lemma for founded recursion. Here, we calculate the value of F (the union of all acceptable functions). (Contributed by Paul Chapman, 21-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 ) ) ) ) ) }   &    |- F = U. B   =>    |- ( y e. dom F -> ( F ` y ) = ( y G ( F |` Pred ( R , A , y ) ) ) )
20.8.21  Surreal Numbers
Syntax	csur 31793	Declare the class of all surreal numbers (see df-no 31796).
class No
Syntax	cslt 31794	Declare the less than relationship over surreal numbers (see df-slt 31797).
class <s
Syntax	cbday 31795	Declare the birthday function for surreal numbers (see df-bday 31798).
class bday
Definition	df-no 31796*	Define the class of surreal numbers. The surreal numbers are a proper class of numbers developed by John H. Conway and introduced by Donald Knuth in 1975. They form a proper class into which all ordered fields can be embedded. The approach we take to defining them was first introduced by Hary Goshnor, and is based on the conception of a "sign expansion" of a surreal number. We define the surreals as ordinal-indexed sequences of 1o and 2o, analagous to Goshnor's ( - ) and ( + ). After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.)
|- No = { f | E. a e. On f : a --> { 1o , 2o } }
Definition	df-slt 31797*	Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.)
|- <s = { <. f , g >. | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }
Definition	df-bday 31798	Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.)
|- bday = ( x e. No |-> dom x )
Theorem	elno 31799*	Membership in the surreals. (Shortened proof on 2012-Apr-14, SF). (Contributed by Scott Fenton, 11-Jun-2011.)
|- ( A e. No <-> E. x e. On A : x --> { 1o , 2o } )
Theorem	sltval 31800*	The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011.)
|- ( ( A e. No /\ B e. No ) -> ( A <s B <-> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )