P. 46 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4501-4600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tz7.2 4501	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 4502	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 4503	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
|- ( R = S -> ( R We A <-> S We A ) )
Theorem	weeq2 4504	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
|- ( A = B -> ( R We A <-> R We B ) )
Theorem	wefr 4505	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
|- ( R We A -> R Fr A )
Theorem	wepo 4506	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 4507*	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 4508	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
|- R We (/)
2.3.10  Ordinals
Syntax	word 4509	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 4510	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 4511	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A
Syntax	csuc 4512	Extend class notation to include the successor function.
class suc A
Definition	df-iord 4513*	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 4514 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Ord A <-> ( Tr A /\ A. x e. A Tr x ) )
Theorem	dford3 4514*	Alias for df-iord 4513. Use it instead of df-iord 4513 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 4515	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 4516	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 4517 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
Theorem	dflim2 4517	Alias for df-ilim 4516. Use it instead of df-ilim 4516 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U. A ) )
Definition	df-suc 4518	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 4559). 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 4519	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
|- ( A = B -> ( Ord A <-> Ord B ) )
Theorem	elong 4520	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- ( A e. V -> ( A e. On <-> Ord A ) )
Theorem	elon 4521	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- A e. _V   =>    |- ( A e. On <-> Ord A )
Theorem	eloni 4522	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
|- ( A e. On -> Ord A )
Theorem	elon2 4523	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|- ( A e. On <-> ( Ord A /\ A e. _V ) )
Theorem	limeq 4524	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 4525	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|- ( Ord A -> Tr A )
Theorem	ordelss 4526	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 4527	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 4528	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 4529	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
|- Tr On
Theorem	ordelon 4530	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 4531	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 4532	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 4533	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 4534	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 4535	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
|- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
Theorem	ontr1 4536	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 4537*	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 4538	The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
|- Ord (/)
Theorem	0elon 4539	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
|- (/) e. On
Theorem	inton 4540	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
|- |^| On = (/)
Theorem	nlim0 4541	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 4542	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
|- ( Lim A -> Ord A )
Theorem	limuni 4543	A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
|- ( Lim A -> A = U. A )
Theorem	limuni2 4544	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
|- ( Lim A -> Lim U. A )
Theorem	0ellim 4545	A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
|- ( Lim A -> (/) e. A )
Theorem	limelon 4546	A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
|- ( ( A e. B /\ Lim A ) -> A e. On )
Theorem	onn0 4547	The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
|- On =/= (/)
Theorem	onm 4548	The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.)
|- E. x x e. On
Theorem	suceq 4549	Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- ( A = B -> suc A = suc B )
Theorem	elsuci 4550	Membership in a successor. This one-way implication does not require that either A or B be sets. (Contributed by NM, 6-Jun-1994.)
|- ( A e. suc B -> ( A e. B \/ A = B ) )
Theorem	elsucg 4551	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
|- ( A e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )
Theorem	elsuc2g 4552	Variant of membership in a successor, requiring that B rather than A be a set. (Contributed by NM, 28-Oct-2003.)
|- ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )
Theorem	elsuc 4553	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
|- A e. _V   =>    |- ( A e. suc B <-> ( A e. B \/ A = B ) )
Theorem	elsuc2 4554	Membership in a successor. (Contributed by NM, 15-Sep-2003.)
|- A e. _V   =>    |- ( B e. suc A <-> ( B e. A \/ B = A ) )
Theorem	nfsuc 4555	Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
|- F/_ x A   =>    |- F/_ x suc A
Theorem	elelsuc 4556	Membership in a successor. (Contributed by NM, 20-Jun-1998.)
|- ( A e. B -> A e. suc B )
Theorem	sucel 4557*	Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
|- ( suc A e. B <-> E. x e. B A. y ( y e. x <-> ( y e. A \/ y = A ) ) )
Theorem	suc0 4558	The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
|- suc (/) = { (/) }
Theorem	sucprc 4559	A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
|- ( -. A e. _V -> suc A = A )
Theorem	unisuc 4560	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- ( Tr A <-> U. suc A = A )
Theorem	unisucg 4561	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
|- ( A e. V -> ( Tr A <-> U. suc A = A ) )
Theorem	sssucid 4562	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
|- A C_ suc A
Theorem	sucidg 4563	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
|- ( A e. V -> A e. suc A )
Theorem	sucid 4564	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
|- A e. _V   =>    |- A e. suc A
Theorem	nsuceq0g 4565	No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.)
|- ( A e. V -> suc A =/= (/) )
Theorem	eqelsuc 4566	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
|- A e. _V   =>    |- ( A = B -> A e. suc B )
Theorem	iunsuc 4567*	Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   &    |- ( x = A -> B = C )   =>    |- U_ x e. suc A B = ( U_ x e. A B u. C )
Theorem	suctr 4568	The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
|- ( Tr A -> Tr suc A )
Theorem	trsuc 4569	A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( ( Tr A /\ suc B e. A ) -> B e. A )
Theorem	trsucss 4570	A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
|- ( Tr A -> ( B e. suc A -> B C_ A ) )
Theorem	sucssel 4571	A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
|- ( A e. V -> ( suc A C_ B -> A e. B ) )
Theorem	orduniss 4572	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
|- ( Ord A -> U. A C_ A )
Theorem	onordi 4573	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Ord A
Theorem	ontrci 4574	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Tr A
Theorem	oneli 4575	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> B e. On )
Theorem	onelssi 4576	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
|- A e. On   =>    |- ( B e. A -> B C_ A )
Theorem	onelini 4577	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> B = ( B i^i A ) )
Theorem	oneluni 4578	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
|- A e. On   =>    |- ( B e. A -> ( A u. B ) = A )
Theorem	onunisuci 4579	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
|- A e. On   =>    |- U. suc A = A
2.4  IZF Set Theory - add the Axiom of Union
2.4.1  Introduce the Axiom of Union
Axiom	ax-un 4580*	Axiom of Union. An axiom of Intuitionistic Zermelo-Fraenkel set theory. It states that a set y exists that includes the union of a given set x i.e. the collection of all members of the members of x. The variant axun2 4582 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4583. A version using class notation is uniex 4585. This is Axiom 3 of [Crosilla] p. "Axioms of CZF and IZF", except (a) unnecessary quantifiers are removed, (b) Crosilla has a biconditional rather than an implication (but the two are equivalent by bm1.3ii 4256), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 266). The union of a class df-uni 3936 should not be confused with the union of two classes df-un 3224. Their relationship is shown in unipr 3949. (Contributed by NM, 23-Dec-1993.)
|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
Theorem	zfun 4581*	Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) (New usage is discouraged.)
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
Theorem	axun2 4582*	A variant of the Axiom of Union ax-un 4580. For any set x, there exists a set y whose members are exactly the members of the members of x i.e. the union of x. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.)
|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
Theorem	uniex2 4583*	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.) (Proof shortened by BJ, 14-Jul-2026.)
|- E. y y = U. x
Theorem	uniex2OLD 4584*	Obsolete version of uniex2 4583 as of 14-Jul-2026. (Contributed by NM, 4-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E. y y = U. x
Theorem	uniex 4585	The Axiom of Union in class notation. This says that if A is a set i.e. A e. _V (see isset 2828), then the union of A is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.)
|- A e. _V   =>    |- U. A e. _V
Theorem	vuniex 4586	The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
|- U. x e. _V
Theorem	uniexg 4587	The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. V instead of A e. _V to make the theorem more general and thus shorten some proofs; obviously the universal class constant _V is one possible substitution for class variable V. (Contributed by NM, 25-Nov-1994.)
|- ( A e. V -> U. A e. _V )
Theorem	uniexd 4588	Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. V )   =>    |- ( ph -> U. A e. _V )
Theorem	unex 4589	The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.)
|- A e. _V   &    |- B e. _V   =>    |- ( A u. B ) e. _V
Theorem	unexb 4590	Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.)
|- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
Theorem	unexg 4591	A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.)
|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
Theorem	tpexg 4592	An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
|- ( ( A e. U /\ B e. V /\ C e. W ) -> { A , B , C } e. _V )
Theorem	unisn3 4593*	Union of a singleton in the form of a restricted class abstraction. (Contributed by NM, 3-Jul-2008.)
|- ( A e. B -> U. { x e. B | x = A } = A )
Theorem	abnexg 4594*	Sufficient condition for a class abstraction to be a proper class. The class F can be thought of as an expression in x and the abstraction appearing in the statement as the class of values F as x varies through A. Assuming the antecedents, if that class is a set, then so is the "domain" A. The converse holds without antecedent, see abrexexg 6351. Note that the second antecedent A. x e. A x e. F cannot be translated to A C_ F since F may depend on x. In applications, one may take F = { x } or F = ~P x (see snnex 4596 and pwnex 4597 respectively, proved from abnex 4595, which is a consequence of abnexg 4594 with A = _V). (Contributed by BJ, 2-Dec-2021.)
|- ( A. x e. A ( F e. V /\ x e. F ) -> ( { y | E. x e. A y = F } e. W -> A e. _V ) )
Theorem	abnex 4595*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4596 and pwnex 4597. See the comment of abnexg 4594. (Contributed by BJ, 2-May-2021.)
|- ( A. x ( F e. V /\ x e. F ) -> -. { y | E. x y = F } e. _V )
Theorem	snnex 4596*	The class of all singletons is a proper class. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.)
|- { x | E. y x = { y } } e/ _V
Theorem	pwnex 4597*	The class of all power sets is a proper class. See also snnex 4596. (Contributed by BJ, 2-May-2021.)
|- { x | E. y x = ~P y } e/ _V
Theorem	opeluu 4598	Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- A e. _V   &    |- B e. _V   =>    |- ( <. A , B >. e. C -> ( A e. U. U. C /\ B e. U. U. C ) )
Theorem	uniuni 4599*	Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.)
|- U. U. A = U. { x | E. y ( x = U. y /\ y e. A ) }
Theorem	eusv1 4600*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 14-Oct-2010.)
|- ( E! y A. x y = A <-> E. y A. x y = A )