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	sucssel 4401	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 4402	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
|- ( Ord A -> U. A C_ A )
Theorem	onordi 4403	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Ord A
Theorem	ontrci 4404	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
|- A e. On   =>    |- Tr A
Theorem	oneli 4405	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 4406	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 4407	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 4408	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 4409	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 4410*	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 4412 states that the union itself exists. A version with the standard abbreviation for union is uniex2 4413. A version using class notation is uniex 4414. 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 4102), and (c) the order of the conjuncts is swapped (which is equivalent by ancom 264). The union of a class df-uni 3789 should not be confused with the union of two classes df-un 3119. Their relationship is shown in unipr 3802. (Contributed by NM, 23-Dec-1993.)
|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
Theorem	zfun 4411*	Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.)
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
Theorem	axun2 4412*	A variant of the Axiom of Union ax-un 4410. 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 4413*	The Axiom of Union using the standard abbreviation for union. Given any set x, its union y exists. (Contributed by NM, 4-Jun-2006.)
|- E. y y = U. x
Theorem	uniex 4414	The Axiom of Union in class notation. This says that if A is a set i.e. A e. _V (see isset 2731), 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 4415	The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
|- U. x e. _V
Theorem	uniexg 4416	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 4417	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 4418	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 4419	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 4420	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 4421	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 4422*	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 4423*	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 6083. 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 4425 and pwnex 4426 respectively, proved from abnex 4424, which is a consequence of abnexg 4423 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 4424*	Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 4425 and pwnex 4426. See the comment of abnexg 4423. (Contributed by BJ, 2-May-2021.)
|- ( A. x ( F e. V /\ x e. F ) -> -. { y | E. x y = F } e. _V )
Theorem	snnex 4425*	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 4426*	The class of all power sets is a proper class. See also snnex 4425. (Contributed by BJ, 2-May-2021.)
|- { x | E. y x = ~P y } e/ _V
Theorem	opeluu 4427	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 4428*	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 4429*	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 )
Theorem	eusvnf 4430*	Even if x is free in A, it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- ( E! y A. x y = A -> F/_ x A )
Theorem	eusvnfb 4431*	Two ways to say that A ( x ) is a set expression that does not depend on x. (Contributed by Mario Carneiro, 18-Nov-2016.)
|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )
Theorem	eusv2i 4432*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 14-Oct-2010.) (Revised by Mario Carneiro, 18-Nov-2016.)
|- ( E! y A. x y = A -> E! y E. x y = A )
Theorem	eusv2nf 4433*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   =>    |- ( E! y E. x y = A <-> F/_ x A )
Theorem	eusv2 4434*	Two ways to express single-valuedness of a class expression A ( x ). (Contributed by NM, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- A e. _V   =>    |- ( E! y E. x y = A <-> E! y A. x y = A )
Theorem	reusv1 4435*	Two ways to express single-valuedness of a class expression C ( y ). (Contributed by NM, 16-Dec-2012.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	reusv3i 4436*	Two ways of expressing existential uniqueness via an indirect equality. (Contributed by NM, 23-Dec-2012.)
|- ( y = z -> ( ph <-> ps ) )   &    |- ( y = z -> C = D )   =>    |- ( E. x e. A A. y e. B ( ph -> x = C ) -> A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) )
Theorem	reusv3 4437*	Two ways to express single-valuedness of a class expression C ( y ). See reusv1 4435 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012.)
|- ( y = z -> ( ph <-> ps ) )   &    |- ( y = z -> C = D )   =>    |- ( E. y e. B ( ph /\ C e. A ) -> ( A. y e. B A. z e. B ( ( ph /\ ps ) -> C = D ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
Theorem	alxfr 4438*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 18-Feb-2007.)
|- ( x = A -> ( ph <-> ps ) )   =>    |- ( ( A. y A e. B /\ A. x E. y x = A ) -> ( A. x ph <-> A. y ps ) )
Theorem	ralxfrd 4439*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 15-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfrd 4440*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by FL, 10-Apr-2007.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( ( ph /\ y e. C ) -> A e. B )   &    |- ( ( ph /\ x e. B ) -> E. y e. C x = A )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
Theorem	ralxfr2d 4441*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.)
|- ( ( ph /\ y e. C ) -> A e. V )   &    |- ( ph -> ( x e. B <-> E. y e. C x = A ) )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. B ps <-> A. y e. C ch ) )
Theorem	rexxfr2d 4442*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- ( ( ph /\ y e. C ) -> A e. V )   &    |- ( ph -> ( x e. B <-> E. y e. C x = A ) )   &    |- ( ( ph /\ x = A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
Theorem	ralxfr 4443*	Transfer universal quantification from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. B ph <-> A. y e. C ps )
Theorem	ralxfrALT 4444*	Transfer universal quantification from a variable x to another variable y contained in expression A. This proof does not use ralxfrd 4439. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x e. B ph <-> A. y e. C ps )
Theorem	rexxfr 4445*	Transfer existence from a variable x to another variable y contained in expression A. (Contributed by NM, 10-Jun-2005.) (Revised by Mario Carneiro, 15-Aug-2014.)
|- ( y e. C -> A e. B )   &    |- ( x e. B -> E. y e. C x = A )   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E. x e. B ph <-> E. y e. C ps )
Theorem	rabxfrd 4446*	Class builder membership after substituting an expression A (containing y) for x in the class expression ch. (Contributed by NM, 16-Jan-2012.)
|- F/_ y B   &    |- F/_ y C   &    |- ( ( ph /\ y e. D ) -> A e. D )   &    |- ( x = A -> ( ps <-> ch ) )   &    |- ( y = B -> A = C )   =>    |- ( ( ph /\ B e. D ) -> ( C e. { x e. D | ps } <-> B e. { y e. D | ch } ) )
Theorem	rabxfr 4447*	Class builder membership after substituting an expression A (containing y) for x in the class expression ph. (Contributed by NM, 10-Jun-2005.)
|- F/_ y B   &    |- F/_ y C   &    |- ( y e. D -> A e. D )   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> A = C )   =>    |- ( B e. D -> ( C e. { x e. D | ph } <-> B e. { y e. D | ps } ) )
Theorem	reuhypd 4448*	A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 16-Jan-2012.)
|- ( ( ph /\ x e. C ) -> B e. C )   &    |- ( ( ph /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) )   =>    |- ( ( ph /\ x e. C ) -> E! y e. C x = A )
Theorem	reuhyp 4449*	A theorem useful for eliminating restricted existential uniqueness hypotheses. (Contributed by NM, 15-Nov-2004.)
|- ( x e. C -> B e. C )   &    |- ( ( x e. C /\ y e. C ) -> ( x = A <-> y = B ) )   =>    |- ( x e. C -> E! y e. C x = A )
Theorem	uniexb 4450	The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.)
|- ( A e. _V <-> U. A e. _V )
Theorem	pwexb 4451	The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.)
|- ( A e. _V <-> ~P A e. _V )
Theorem	elpwpwel 4452	A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.)
|- ( A e. ~P ~P B <-> U. A e. ~P B )
Theorem	univ 4453	The union of the universe is the universe. Exercise 4.12(c) of [Mendelson] p. 235. (Contributed by NM, 14-Sep-2003.)
|- U. _V = _V
Theorem	eldifpw 4454	Membership in a power class difference. (Contributed by NM, 25-Mar-2007.)
|- C e. _V   =>    |- ( ( A e. ~P B /\ -. C C_ B ) -> ( A u. C ) e. ( ~P ( B u. C ) \ ~P B ) )
Theorem	op1stb 4455	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by NM, 25-Nov-2003.)
|- A e. _V   &    |- B e. _V   =>    |- |^| |^| <. A , B >. = A
Theorem	op1stbg 4456	Extract the first member of an ordered pair. Theorem 73 of [Suppes] p. 42. (Contributed by Jim Kingdon, 17-Dec-2018.)
|- ( ( A e. V /\ B e. W ) -> |^| |^| <. A , B >. = A )
Theorem	iunpw 4457*	An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.)
|- A e. _V   =>    |- ( E. x e. A x = U. A <-> ~P U. A = U_ x e. A ~P x )
Theorem	ifelpwung 4458	Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
|- ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. ~P ( A u. B ) )
Theorem	ifelpwund 4459	Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ps , A , B ) e. ~P ( A u. B ) )
Theorem	ifelpwun 4460	Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
|- A e. _V   &    |- B e. _V   =>    |- if ( ph , A , B ) e. ~P ( A u. B )
Theorem	ifexd 4461	Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> if ( ps , A , B ) e. _V )
2.4.2  Ordinals (continued)
Theorem	ordon 4462	The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
|- Ord On
Theorem	ssorduni 4463	The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- ( A C_ On -> Ord U. A )
Theorem	ssonuni 4464	The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.)
|- ( A e. V -> ( A C_ On -> U. A e. On ) )
Theorem	ssonunii 4465	The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.)
|- A e. _V   =>    |- ( A C_ On -> U. A e. On )
Theorem	onun2 4466	The union of two ordinal numbers is an ordinal number. (Contributed by Jim Kingdon, 25-Jul-2019.)
|- ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On )
Theorem	onun2i 4467	The union of two ordinal numbers is an ordinal number. (Contributed by NM, 13-Jun-1994.) (Constructive proof by Jim Kingdon, 25-Jul-2019.)
|- A e. On   &    |- B e. On   =>    |- ( A u. B ) e. On
Theorem	ordsson 4468	Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.)
|- ( Ord A -> A C_ On )
Theorem	onss 4469	An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.)
|- ( A e. On -> A C_ On )
Theorem	onuni 4470	The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
|- ( A e. On -> U. A e. On )
Theorem	orduni 4471	The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.)
|- ( Ord A -> Ord U. A )
Theorem	bm2.5ii 4472*	Problem 2.5(ii) of [BellMachover] p. 471. (Contributed by NM, 20-Sep-2003.)
|- A e. _V   =>    |- ( A C_ On -> U. A = |^| { x e. On | A. y e. A y C_ x } )
Theorem	sucexb 4473	A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998.)
|- ( A e. _V <-> suc A e. _V )
Theorem	sucexg 4474	The successor of a set is a set (generalization). (Contributed by NM, 5-Jun-1994.)
|- ( A e. V -> suc A e. _V )
Theorem	sucex 4475	The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
|- A e. _V   =>    |- suc A e. _V
Theorem	ordsucim 4476	The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 8-Nov-2018.)
|- ( Ord A -> Ord suc A )
Theorem	suceloni 4477	The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
|- ( A e. On -> suc A e. On )
Theorem	ordsucg 4478	The successor of an ordinal class is ordinal. (Contributed by Jim Kingdon, 20-Nov-2018.)
|- ( A e. _V -> ( Ord A <-> Ord suc A ) )
Theorem	sucelon 4479	The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003.)
|- ( A e. On <-> suc A e. On )
Theorem	ordsucss 4480	The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.)
|- ( Ord B -> ( A e. B -> suc A C_ B ) )
Theorem	ordelsuc 4481	A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 29-Nov-2003.)
|- ( ( A e. C /\ Ord B ) -> ( A e. B <-> suc A C_ B ) )
Theorem	onsucssi 4482	A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of [TakeutiZaring] p. 42 and its converse. (Contributed by NM, 16-Sep-1995.)
|- A e. On   &    |- B e. On   =>    |- ( A e. B <-> suc A C_ B )
Theorem	onsucmin 4483*	The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003.)
|- ( A e. On -> suc A = |^| { x e. On | A e. x } )
Theorem	onsucelsucr 4484	Membership is inherited by predecessors. The converse, for all ordinals, implies excluded middle, as shown at onsucelsucexmid 4506. However, the converse does hold where B is a natural number, as seen at nnsucelsuc 6455. (Contributed by Jim Kingdon, 17-Jul-2019.)
|- ( B e. On -> ( suc A e. suc B -> A e. B ) )
Theorem	onsucsssucr 4485	The subclass relationship between two ordinals is inherited by their predecessors. The converse implies excluded middle, as shown at onsucsssucexmid 4503. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2019.)
|- ( ( A e. On /\ Ord B ) -> ( suc A C_ suc B -> A C_ B ) )
Theorem	sucunielr 4486	Successor and union. The converse (where B is an ordinal) implies excluded middle, as seen at ordsucunielexmid 4507. (Contributed by Jim Kingdon, 2-Aug-2019.)
|- ( suc A e. B -> A e. U. B )
Theorem	unon 4487	The class of all ordinal numbers is its own union. Exercise 11 of [TakeutiZaring] p. 40. (Contributed by NM, 12-Nov-2003.)
|- U. On = On
Theorem	onuniss2 4488*	The union of the ordinal subsets of an ordinal number is that number. (Contributed by Jim Kingdon, 2-Aug-2019.)
|- ( A e. On -> U. { x e. On | x C_ A } = A )
Theorem	limon 4489	The class of ordinal numbers is a limit ordinal. (Contributed by NM, 24-Mar-1995.)
|- Lim On
Theorem	ordunisuc2r 4490*	An ordinal which contains the successor of each of its members is equal to its union. (Contributed by Jim Kingdon, 14-Nov-2018.)
|- ( Ord A -> ( A. x e. A suc x e. A -> A = U. A ) )
Theorem	onssi 4491	An ordinal number is a subset of On. (Contributed by NM, 11-Aug-1994.)
|- A e. On   =>    |- A C_ On
Theorem	onsuci 4492	The successor of an ordinal number is an ordinal number. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)
|- A e. On   =>    |- suc A e. On
Theorem	onintonm 4493*	The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)
|- ( ( A C_ On /\ E. x x e. A ) -> |^| A e. On )
Theorem	onintrab2im 4494	An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( E. x e. On ph -> |^| { x e. On | ph } e. On )
Theorem	ordtriexmidlem 4495	Lemma for decidability and ordinals. The set { x e. { (/) } | ph } is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4497 or weak linearity in ordsoexmid 4538) with a proposition ph. Our lemma states that it is an ordinal number. (Contributed by Jim Kingdon, 28-Jan-2019.)
|- { x e. { (/) } | ph } e. On
Theorem	ordtriexmidlem2 4496*	Lemma for decidability and ordinals. The set { x e. { (/) } | ph } is a way of connecting statements about ordinals (such as trichotomy in ordtriexmid 4497 or weak linearity in ordsoexmid 4538) with a proposition ph. Our lemma helps connect that set to excluded middle. (Contributed by Jim Kingdon, 28-Jan-2019.)
|- ( { x e. { (/) } | ph } = (/) -> -. ph )
Theorem	ordtriexmid 4497*	Ordinal trichotomy implies the law of the excluded middle (that is, decidability of an arbitrary proposition). This theorem is stated in "Constructive ordinals", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Also see exmidontri 7191 which is much the same theorem but biconditionalized and using the EXMID notation. (Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.)
|- A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x )   =>    |- ( ph \/ -. ph )
Theorem	ontriexmidim 4498*	Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4497. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- ( A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> DECID ph )
Theorem	ordtri2orexmid 4499*	Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 31-Jul-2019.)
|- A. x e. On A. y e. On ( x e. y \/ y C_ x )   =>    |- ( ph \/ -. ph )
Theorem	2ordpr 4500	Version of 2on 6389 with the definition of 2o expanded and expressed in terms of Ord. (Contributed by Jim Kingdon, 29-Aug-2021.)
|- Ord { (/) , { (/) } }