P. 45 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	poss 4401	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 4402	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A ) )
Theorem	poeq2 4403	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( A = B -> ( R Po A <-> R Po B ) )
Theorem	nfpo 4404	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 4405	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 4406	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 4407*	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 4408*	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 4409*	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 4410	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- ( ( R Po A /\ B e. A ) -> -. B R B )
Theorem	potr 4411	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 4412	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 4413	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 4414	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 4415*	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 4416	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A )
Theorem	soss 4417	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 4418	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A ) )
Theorem	soeq2 4419	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( A = B -> ( R Or A <-> R Or B ) )
Theorem	sonr 4420	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- ( ( R Or A /\ B e. A ) -> -. B R B )
Theorem	sotr 4421	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 4422*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4400). (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 4423	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 4424	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 4425	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 4426	One direction of sotritric 4427 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 4427	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 4428	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 4429	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 4430	Extend wff notation to include the well-founded predicate.
wff FrFor R A S
Syntax	wfr 4431	Extend wff notation to include the well-founded predicate. Read: ' R is a well-founded relation on A.'
wff R Fr A
Syntax	wse 4432	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Syntax	wwe 4433	Extend wff notation to include the well-ordering predicate. Read: ' R well-orders A.'
wff R We A
Definition	df-frfor 4434*	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 4435*	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 4436*	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 4437*	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 do not have that as seen at ordtriexmid 4625). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition 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 4438*	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 4439	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 4440	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 4441	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 4442	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A ) )
Theorem	seeq2 4443	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( A = B -> ( R Se A <-> R Se B ) )
Theorem	nfse 4444	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 4445	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 4446	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 4447	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R Fr A <-> S Fr A ) )
Theorem	frforeq2 4448	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 4449	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R Fr A <-> R Fr B ) )
Theorem	frforeq3 4450	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 4451	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 4452	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 4453	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 4454	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
|- R Fr (/)
Theorem	frind 4455*	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 4456	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 4457	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 4458	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 4459	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R We A <-> S We A ) )
Theorem	weeq2 4460	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R We A <-> R We B ) )
Theorem	wefr 4461	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|- ( R We A -> R Fr A )
Theorem	wepo 4462	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 4463*	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 4464	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
|- R We (/)
2.3.10  Ordinals
Syntax	word 4465	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 4466	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
Syntax	wlim 4467	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A
Syntax	csuc 4468	Extend class notation to include the successor function.
class suc A
Definition	df-iord 4469*	Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Some sources will define a notation for ordinal order corresponding to < and <_ but we just use e. and C_ respectively. (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4470 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
Theorem	dford3 4470*	Alias for df-iord 4469. Use it instead of df-iord 4469 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
Definition	df-on 4471	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
|- On = { x | Ord x }
Definition	df-ilim 4472	Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes A =/= (/) to (/) e. A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4473 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
Theorem	dflim2 4473	Alias for df-ilim 4472. Use it instead of df-ilim 4472 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
Definition	df-suc 4474	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4515). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
|- suc A = ( A u. { A } )
Theorem	ordeq 4475	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Ord A <-> Ord B ) )
Theorem	elong 4476	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- ( A e. V -> ( A e. On <-> Ord A ) )
Theorem	elon 4477	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- A e. _V   =>    |- ( A e. On <-> Ord A )
Theorem	eloni 4478	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
|- ( A e. On -> Ord A )
Theorem	elon2 4479	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|- ( A e. On <-> ( Ord A /\ A e. _V ) )
Theorem	limeq 4480	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A = B -> ( Lim A <-> Lim B ) )
Theorem	ordtr 4481	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|- ( Ord A -> Tr A )
Theorem	ordelss 4482	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
|- ( ( Ord A /\ B e. A ) -> B C_ A )
Theorem	trssord 4483	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
|- ( ( Tr A /\ A C_ B /\ Ord B ) -> Ord A )
Theorem	ordelord 4484	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
|- ( ( Ord A /\ B e. A ) -> Ord B )
Theorem	tron 4485	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
|- Tr On
Theorem	ordelon 4486	An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
|- ( ( Ord A /\ B e. A ) -> B e. On )
Theorem	onelon 4487	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
|- ( ( A e. On /\ B e. A ) -> B e. On )
Theorem	ordin 4488	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
|- ( ( Ord A /\ Ord B ) -> Ord ( A i^i B ) )
Theorem	onin 4489	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
|- ( ( A e. On /\ B e. On ) -> ( A i^i B ) e. On )
Theorem	onelss 4490	An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A e. On -> ( B e. A -> B C_ A ) )
Theorem	ordtr1 4491	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
|- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
Theorem	ontr1 4492	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
|- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) )
Theorem	onintss 4493*	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. On -> ( ps -> |^| { x e. On | ph } C_ A ) )
Theorem	ord0 4494	The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
|- Ord (/)
Theorem	0elon 4495	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
|- (/) e. On
Theorem	inton 4496	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
|- |^| On = (/)
Theorem	nlim0 4497	The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- -. Lim (/)
Theorem	limord 4498	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
|- ( Lim A -> Ord A )
Theorem	limuni 4499	A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
|- ( Lim A -> A = U. A )
Theorem	limuni2 4500	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
|- ( Lim A -> Lim U. A )