P. 42 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4101-4200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opcom 4101	An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. = <. B , A >. <-> A = B )
Theorem	moop2 4102*	"At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- B e. _V   =>    |- E* x A = <. B , x >.
Theorem	opeqsn 4103	Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   =>    |- ( <. A , B >. = { C } <-> ( A = B /\ C = { A } ) )
Theorem	opeqpr 4104	Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- D e. _V   =>    |- ( <. A , B >. = { C , D } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) )
Theorem	euotd 4105*	Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ph -> C e. _V )   &    |- ( ph -> ( ps <-> ( a = A /\ b = B /\ c = C ) ) )   =>    |- ( ph -> E! x E. a E. b E. c ( x = <. a , b , c >. /\ ps ) )
Theorem	uniop 4106	The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- U. <. A , B >. = { A , B }
Theorem	uniopel 4107	Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. C -> U. <. A , B >. e. U. C )
2.3.5  Ordered-pair class abstractions (cont.)
Theorem	opabid 4108	The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
Theorem	elopab 4109*	Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
|- ( A e. { <. x , y >. | ph } <-> E. x E. y ( A = <. x , y >. /\ ph ) )
Theorem	opelopabsbALT 4110*	The law of concretion in terms of substitutions. Less general than opelopabsb 4111, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( <. z , w >. e. { <. x , y >. | ph } <-> [ w / y ] [ z / x ] ph )
Theorem	opelopabsb 4111*	The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )
Theorem	brabsb 4112*	The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
|- R = { <. x , y >. | ph }   =>    |- ( A R B <-> [. A / x ]. [. B / y ]. ph )
Theorem	opelopabt 4113*	Closed theorem form of opelopab 4122. (Contributed by NM, 19-Feb-2013.)
|- ( ( A. x A. y ( x = A -> ( ph <-> ps ) ) /\ A. x A. y ( y = B -> ( ps <-> ch ) ) /\ ( A e. V /\ B e. W ) ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ch ) )
Theorem	opelopabga 4114*	The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )   =>    |- ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) )
Theorem	brabga 4115*	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 4116*	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 4117*	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 4118*	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 4119*	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 4120*	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 4121*	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 4122*	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 4123*	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 4124*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4122 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 4125*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4122 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 4126	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 4127	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 4128	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 4129*	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 4130	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 4131*	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 4132*	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.6  Power class of union and intersection
Theorem	pwin 4133	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 4134	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 4135	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 4136	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 4137	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.7  Epsilon and identity relations
Syntax	cep 4138	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 4139	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 4140*	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 4141. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
|- _E = { <. x , y >. | x e. y }
Theorem	epelg 4141	The epsilon relation and membership are the same. General version of epel 4143. (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 4142	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 4143	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 4144*	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.8  Partial and complete ordering
Syntax	wpo 4145	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 4146	Extend wff notation to include the strict linear ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 4147*	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 4148*	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 4149	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 4150	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 4151	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 4152	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 4153	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 4154	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 4155*	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 4156*	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 4157*	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 4158	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 4159	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 4160	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 4161	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 4162	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 4163*	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 4164	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 4165	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 4166	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 4167	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 4168	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 4169	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 4170*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4148). (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 4171	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 4172	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 4173	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 4174	One direction of sotritric 4175 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 4175	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 4176	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 4177	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.9  Founded and set-like relations
Syntax	wfrfor 4178	Extend wff notation to include the well-founded predicate.
wff FrFor R A S
Syntax	wfr 4179	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 4180	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 4181	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-frfor 4182*	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 4183*	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 4184*	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 4185*	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 4366). 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 4186*	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 4187	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 4188	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 4189	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 4190	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 4191	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nfse 4192	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 4193	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 4194	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 4195	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	frforeq2 4196	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 4197	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	frforeq3 4198	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 4199	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 4200	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