P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	brabga 4001*	The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )
Theorem	opelopab2a 4002*	Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ps ) )
Theorem	opelopaba 4003*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps )
Theorem	braba 4004*	The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( A R B <-> ps )
Theorem	opelopabg 4005*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	brabg 4006*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( ( A e. C /\ B e. D ) -> ( A R B <-> ch ) )
Theorem	opelopab2 4007*	Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ch ) )
Theorem	opelopab 4008*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ch )
Theorem	brab 4009*	The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
|- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- R = { <. x , y >. | ph }   =>    |- ( A R B <-> ch )
Theorem	opelopabaf 4010*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4008 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- F/ x ps   &    |- F/ y ps   &    |- A e. _V   &    |- B e. _V   &    |- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ps )
Theorem	opelopabf 4011*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4008 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
|- F/ x ps   &    |- F/ y ch   &    |- A e. _V   &    |- B e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   =>    |- ( <. A , B >. e. { <. x , y >. | ph } <-> ch )
Theorem	ssopab2 4012	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
|- ( A. x A. y ( ph -> ps ) -> { <. x , y >. | ph } C_ { <. x , y >. | ps } )
Theorem	ssopab2b 4013	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( { <. x , y >. | ph } C_ { <. x , y >. | ps } <-> A. x A. y ( ph -> ps ) )
Theorem	ssopab2i 4014	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
|- ( ph -> ps )   =>    |- { <. x , y >. | ph } C_ { <. x , y >. | ps }
Theorem	ssopab2dv 4015*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> { <. x , y >. | ps } C_ { <. x , y >. | ch } )
Theorem	eqopab2b 4016	Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( { <. x , y >. | ph } = { <. x , y >. | ps } <-> A. x A. y ( ph <-> ps ) )
Theorem	opabm 4017*	Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
|- ( E. z z e. { <. x , y >. | ph } <-> E. x E. y ph )
Theorem	iunopab 4018*	Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- U_ z e. A { <. x , y >. | ph } = { <. x , y >. | E. z e. A ph }
2.3.5  Power class of union and intersection
Theorem	pwin 4019	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ~P ( A i^i B ) = ( ~P A i^i ~P B )
Theorem	pwunss 4020	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ( ~P A u. ~P B ) C_ ~P ( A u. B )
Theorem	pwssunim 4021	The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ( ( A C_ B \/ B C_ A ) -> ~P ( A u. B ) C_ ( ~P A u. ~P B ) )
Theorem	pwundifss 4022	Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ( ( ~P ( A u. B ) \ ~P A ) u. ~P A ) C_ ~P ( A u. B )
Theorem	pwunim 4023	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ( ( A C_ B \/ B C_ A ) -> ~P ( A u. B ) = ( ~P A u. ~P B ) )
2.3.6  Epsilon and identity relations
Syntax	cep 4024	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 4025	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 4026*	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, ( A _E B <-> A e. B ) when B is a set by epelg 4027. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
|- _E = { <. x , y >. | x e. y }
Theorem	epelg 4027	The epsilon relation and membership are the same. General version of epel 4029. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( B e. V -> ( A _E B <-> A e. B ) )
Theorem	epelc 4028	The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
|- B e. _V   =>    |- ( A _E B <-> A e. B )
Theorem	epel 4029	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
|- ( x _E y <-> x e. y )
Definition	df-id 4030*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 _I 5 and -. 4 _I 5. (Contributed by NM, 13-Aug-1995.)
|- _I = { <. x , y >. | x = y }
2.3.7  Partial and complete ordering
Syntax	wpo 4031	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 4032	Extend wff notation to include the strict linear ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 4033*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression R Po A means R is a partial order on A. (Contributed by NM, 16-Mar-1997.)
|- ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
Definition	df-iso 4034*	Define the strict linear order predicate. The expression R Or A is true if relationship R orders A. The property x R y -> ( x R z \/ z R y ) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, x R y \/ x = y \/ y R x. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ z R y ) ) ) )
Theorem	poss 4035	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( A C_ B -> ( R Po B -> R Po A ) )
Theorem	poeq1 4036	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 4037	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 4038	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Po A
Theorem	nfso 4039	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Or A
Theorem	pocl 4040	Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
|- ( R Po A -> ( ( B e. A /\ C e. A /\ D e. A ) -> ( -. B R B /\ ( ( B R C /\ C R D ) -> B R D ) ) ) )
Theorem	ispod 4041*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
|- ( ( ph /\ x e. A ) -> -. x R x )   &    |- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R y /\ y R z ) -> x R z ) )   =>    |- ( ph -> R Po A )
Theorem	swopolem 4042*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )   =>    |- ( ( ph /\ ( X e. A /\ Y e. A /\ Z e. A ) ) -> ( X R Y -> ( X R Z \/ Z R Y ) ) )
Theorem	swopo 4043*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( y R z -> -. z R y ) )   &    |- ( ( ph /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R y -> ( x R z \/ z R y ) ) )   =>    |- ( ph -> R Po A )
Theorem	poirr 4044	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 4045	A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
Theorem	po2nr 4046	A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
Theorem	po3nr 4047	A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
Theorem	po0 4048	Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Po (/)
Theorem	pofun 4049*	A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
|- S = { <. x , y >. | X R Y }   &    |- ( x = y -> X = Y )   =>    |- ( ( R Po B /\ A. x e. A X e. B ) -> S Po A )
Theorem	sopo 4050	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 4051	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A C_ B -> ( R Or B -> R Or A ) )
Theorem	soeq1 4052	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 4053	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 4054	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 4055	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( B R C /\ C R D ) -> B R D ) )
Theorem	issod 4056*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4034). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- ( ph -> R Po A )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( x R y \/ x = y \/ y R x ) )   =>    |- ( ph -> R Or A )
Theorem	sowlin 4057	A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( B R C -> ( B R D \/ D R C ) ) )
Theorem	so2nr 4058	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )
Theorem	so3nr 4059	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- ( ( R Or A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )
Theorem	sotricim 4060	One direction of sotritric 4061 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C -> -. ( B = C \/ C R B ) ) )
Theorem	sotritric 4061	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- R Or A   &    |- ( ( B e. A /\ C e. A ) -> ( B R C \/ B = C \/ C R B ) )   =>    |- ( ( B e. A /\ C e. A ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )
Theorem	sotritrieq 4062	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- R Or A   &    |- ( ( B e. A /\ C e. A ) -> ( B R C \/ B = C \/ C R B ) )   =>    |- ( ( B e. A /\ C e. A ) -> ( B = C <-> -. ( B R C \/ C R B ) ) )
Theorem	so0 4063	Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Or (/)
2.3.8  Founded and set-like relations
Syntax	wfrfor 4064	Extend wff notation to include the well-founded predicate.
wff FrFor R A S
Syntax	wfr 4065	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 4066	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 4067	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-frfor 4068*	Define the well-founded relation predicate where A might be a proper class. By passing in S we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
|- (FrFor R A S <-> ( A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S ) -> A C_ S ) )
Definition	df-frind 4069*	Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because s is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
|- ( R Fr A <-> A. sFrFor R A s )
Definition	df-se 4070*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )
Definition	df-wetr 4071*	Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4247). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
|- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )
Theorem	seex 4072*	The R-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )
Theorem	exse 4073	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- ( A e. V -> R Se A )
Theorem	sess1 4074	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R C_ S -> ( S Se A -> R Se A ) )
Theorem	sess2 4075	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A C_ B -> ( R Se B -> R Se A ) )
Theorem	seeq1 4076	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 4077	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nfse 4078	Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Se A
Theorem	epse 4079	The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
|- _E Se A
Theorem	frforeq1 4080	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( R = S -> (FrFor R A T <-> FrFor S A T ) )
Theorem	freq1 4081	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	frforeq2 4082	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( A = B -> (FrFor R A T <-> FrFor R B T ) )
Theorem	freq2 4083	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	frforeq3 4084	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
|- ( S = T -> (FrFor R A S <-> FrFor R A T ) )
Theorem	nffrfor 4085	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   &    |- F/_ x S   =>    |- F/ xFrFor R A S
Theorem	nffr 4086	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R Fr A
Theorem	frirrg 4087	A well-founded relation is irreflexive. This is the case where A exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
|- ( ( R Fr A /\ A e. V /\ B e. A ) -> -. B R B )
Theorem	fr0 4088	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
|- R Fr (/)
Theorem	frind 4089*	Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( ( ch /\ x e. A ) -> ( A. y e. A ( y R x -> ps ) -> ph ) )   &    |- ( ch -> R Fr A )   &    |- ( ch -> A e. V )   =>    |- ( ( ch /\ x e. A ) -> ph )
Theorem	efrirr 4090	Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
|- ( _E Fr A -> -. A e. A )
Theorem	tz7.2 4091	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent _E Fr A. (Contributed by NM, 4-May-1994.)
|- ( ( Tr A /\ _E Fr A /\ B e. A ) -> ( B C_ A /\ B =/= A ) )
Theorem	nfwe 4092	Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x R   &    |- F/_ x A   =>    |- F/ x R We A
Theorem	weeq1 4093	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R We A <-> S We A ) )
Theorem	weeq2 4094	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R We A <-> R We B ) )
Theorem	wefr 4095	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|- ( R We A -> R Fr A )
Theorem	wepo 4096	A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
|- ( ( R We A /\ A e. V ) -> R Po A )
Theorem	wetrep 4097*	An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
|- ( ( _E We A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x e. y /\ y e. z ) -> x e. z ) )
Theorem	we0 4098	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
|- R We (/)
2.3.9  Ordinals
Syntax	word 4099	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 4100	Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On