P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nninfdcinf 7501*	The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( ph -> om e. WOmni )   &    |- ( ph -> N e. ℕ∞ )   =>    |- ( ph -> DECID N = ( i e. om |-> 1o ) )
Theorem	nninfwlporlemd 7502*	Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   =>    |- ( ph -> ( X = Y <-> D = ( i e. om |-> 1o ) ) )
Theorem	nninfwlporlem 7503*	Lemma for nninfwlpor 7504. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( ph -> X : om --> 2o )   &    |- ( ph -> Y : om --> 2o )   &    |- D = ( i e. om |-> if ( ( X ` i ) = ( Y ` i ) , 1o , (/) ) )   &    |- ( ph -> om e. WOmni )   =>    |- ( ph -> DECID X = Y )
Theorem	nninfwlpor 7504*	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
|- ( om e. WOmni -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )
Theorem	nninfwlpoimlemg 7505*	Lemma for nninfwlpoim 7509. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> G e. ℕ∞ )
Theorem	nninfwlpoimlemginf 7506*	Lemma for nninfwlpoim 7509. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   =>    |- ( ph -> ( G = ( i e. om |-> 1o ) <-> A. n e. om ( F ` n ) = 1o ) )
Theorem	nninfwlpoimlemdc 7507*	Lemma for nninfwlpoim 7509. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   &    |- ( ph -> A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y )   =>    |- ( ph -> DECID A. n e. om ( F ` n ) = 1o )
Theorem	nninfinfwlpolem 7508*	Lemma for nninfinfwlpo 7510. (Contributed by Jim Kingdon, 8-Dec-2024.)
|- ( ph -> F : om --> 2o )   &    |- G = ( i e. om |-> if ( E. x e. suc i ( F ` x ) = (/) , (/) , 1o ) )   &    |- ( ph -> A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) )   =>    |- ( ph -> DECID A. n e. om ( F ` n ) = 1o )
Theorem	nninfwlpoim 7509*	Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y -> om e. WOmni )
Theorem	nninfinfwlpo 7510*	The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7463). (Contributed by Jim Kingdon, 25-Nov-2025.)
|- ( A. x e. ℕ∞ DECID x = ( i e. om |-> 1o ) <-> om e. WOmni )
Theorem	nninfwlpo 7511*	Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
|- ( A. x e. ℕ∞ A. y e. ℕ∞ DECID x = y <-> om e. WOmni )
2.6.44  Cardinal numbers
Syntax	ccrd 7512	Extend class definition to include the cardinal size function.
class card
Syntax	wacn 7513	The axiom of choice for limited-length sequences.
class AC A
Definition	df-card 7514*	Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)
|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
Definition	df-acnm 7515*	Define a local and length-limited version of the axiom of choice. The definition of the predicate X e. AC A is that for all families of inhabited subsets of X indexed on A (i.e. functions A --> { z e. ~P X | E. j j e. z }), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)
|- AC A = { x | ( A e. _V /\ A. f e. ( { z e. ~P x | E. j j e. z } ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
Theorem	cardcl 7516*	The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( E. y e. On y ~~ A -> ( card ` A ) e. On )
Theorem	isnumi 7517	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. On /\ A ~~ B ) -> B e. dom card )
Theorem	finnum 7518	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. Fin -> A e. dom card )
Theorem	onenon 7519	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- ( A e. On -> A e. dom card )
Theorem	cardval3ex 7520*	The value of ( card ` A ). (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( E. x e. On x ~~ A -> ( card ` A ) = |^| { y e. On | y ~~ A } )
Theorem	oncardval 7521*	The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
|- ( A e. On -> ( card ` A ) = |^| { x e. On | x ~~ A } )
Theorem	cardonle 7522	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)
|- ( A e. On -> ( card ` A ) C_ A )
Theorem	card0 7523	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
|- ( card ` (/) ) = (/)
Theorem	ficardon 7524	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
|- ( A e. Fin -> ( card ` A ) e. On )
Theorem	carden2bex 7525*	If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( ( A ~~ B /\ E. x e. On x ~~ A ) -> ( card ` A ) = ( card ` B ) )
Theorem	pm54.43 7526	Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
|- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )
Theorem	pr2nelem 7527	Lemma for pr2ne 7528. (Contributed by FL, 17-Aug-2008.)
|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )
Theorem	pr2ne 7528	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )
Theorem	en2prde 7529*	A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by Jim Kingdon, 11-Jan-2026.)
|- ( V ~~ 2o -> E. a E. b ( a =/= b /\ V = { a , b } ) )
Theorem	pr1or2 7530	An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.)
|- ( ( A e. C /\ B e. D /\ DECID A = B ) -> ( { A , B } ~~ 1o \/ { A , B } ~~ 2o ) )
Theorem	pr2cv1 7531	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
|- ( { A , B } ~~ 2o -> A e. _V )
Theorem	pr2cv2 7532	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
|- ( { A , B } ~~ 2o -> B e. _V )
Theorem	pr2cv 7533	If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.)
|- ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) )
Theorem	sspw1or2 7534*	The set of subsets of a given set with one or two elements can be expressed as elements of the power set or as inhabited elements of the power set. (Contributed by Jim Kingdon, 31-Mar-2026.)
|- { x e. { s e. ~P V | E. j j e. s } | ( x ~~ 1o \/ x ~~ 2o ) } = { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) }
Theorem	exmidonfinlem 7535*	Lemma for exmidonfin 7536. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- A = { { x e. { (/) } | ph } , { x e. { (/) } | -. ph } }   =>    |- ( om = ( On i^i Fin ) -> DECID ph )
Theorem	exmidonfin 7536	If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 7164 and nnon 4752. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- ( om = ( On i^i Fin ) -> EXMID )
Theorem	en2eleq 7537	Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } )
Theorem	en2other2 7538	Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X )
Theorem	dju1p1e2 7539	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( 1o ⊔ 1o ) ~~ 2o
Theorem	infpwfidom 7540	The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption ( ~P A i^i Fin ) e. _V because this theorem also implies that A is a set if ~P A i^i Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )
Theorem	exmidfodomrlemeldju 7541	Lemma for exmidfodomr 7546. A variant of djur 7399. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( ph -> A C_ 1o )   &    |- ( ph -> B e. ( A ⊔ 1o ) )   =>    |- ( ph -> ( B = (inl ` (/) ) \/ B = (inr ` (/) ) ) )
Theorem	exmidfodomrlemreseldju 7542	Lemma for exmidfodomrlemrALT 7545. A variant of eldju 7398. (Contributed by Jim Kingdon, 9-Jul-2022.)
|- ( ph -> A C_ 1o )   &    |- ( ph -> B e. ( A ⊔ 1o ) )   =>    |- ( ph -> ( ( (/) e. A /\ B = ( (inl |` A ) ` (/) ) ) \/ B = ( (inr |` 1o ) ` (/) ) ) )
Theorem	exmidfodomrlemim 7543*	Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- (EXMID -> A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) )
Theorem	exmidfodomrlemr 7544*	The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> EXMID )
Theorem	exmidfodomrlemrALT 7545*	The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7544. In particular, this proof uses eldju 7398 instead of djur 7399 and avoids djulclb 7385. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
|- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> EXMID )
Theorem	exmidfodomr 7546*	Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- (EXMID <-> A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) )
Theorem	acnrcl 7547	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( X e. AC A -> A e. _V )
Theorem	acneq 7548	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A = C -> AC A = AC C )
Theorem	isacnm 7549*	The property of being a choice set of length A. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( ( X e. V /\ A e. W ) -> ( X e. AC A <-> A. f e. ( { z e. ~P X | E. j j e. z } ^m A ) E. g A. x e. A ( g ` x ) e. ( f ` x ) ) )
Theorem	finacn 7550	Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A e. Fin -> AC A = _V )
2.6.45  Axiom of Choice equivalents
Syntax	wac 7551	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7552*	The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49. There are some decisions about how to write this definition especially around whether ax-setind 4679 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
Theorem	acfun 7553*	A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
|- ( ph -> CHOICE )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. x e. A E. w w e. x )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) )
Theorem	exmidaclem 7554*	Lemma for exmidac 7555. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }   &    |- C = { A , B }   =>    |- (CHOICE -> EXMID )
Theorem	exmidac 7555	The axiom of choice implies excluded middle. See acexmid 6074 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- (CHOICE -> EXMID )
2.6.46  Cardinal number arithmetic
Theorem	endjudisj 7556	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( A ⊔ B ) ~~ ( A u. B ) )
Theorem	djuen 7557	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7558	Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A ⊔ C ) ~~ ( B u. D ) )
Theorem	dju1en 7559	Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ -. A e. A ) -> ( A ⊔ 1o ) ~~ suc A )
Theorem	dju0en 7560	Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. V -> ( A ⊔ (/) ) ~~ A )
Theorem	xp2dju 7561	Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( 2o X. A ) = ( A ⊔ A )
Theorem	djucomen 7562	Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) ~~ ( B ⊔ A ) )
Theorem	djuassen 7563	Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ⊔ B ) ⊔ C ) ~~ ( A ⊔ ( B ⊔ C ) ) )
Theorem	xpdjuen 7564	Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. ( B ⊔ C ) ) ~~ ( ( A X. B ) ⊔ ( A X. C ) ) )
Theorem	djudoml 7565	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> A ~<_ ( A ⊔ B ) )
Theorem	djudomr 7566	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> B ~<_ ( A ⊔ B ) )
2.6.47  Ordinal trichotomy
Theorem	exmidontriimlem1 7567	Lemma for exmidontriim 7571. A variation of r19.30dc 2698. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ( A. x e. A ( ph \/ ps \/ ch ) /\ EXMID ) -> ( E. x e. A ph \/ E. x e. A ps \/ A. x e. A ch ) )
Theorem	exmidontriimlem2 7568*	Lemma for exmidontriim 7571. (Contributed by Jim Kingdon, 12-Aug-2024.)
|- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A. y e. B y e. A ) )
Theorem	exmidontriimlem3 7569*	Lemma for exmidontriim 7571. What we get to do based on induction on both A and B. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   &    |- ( ph -> A. y e. B ( A e. y \/ A = y \/ y e. A ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	exmidontriimlem4 7570*	Lemma for exmidontriim 7571. The induction step for the induction on A. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> EXMID )   &    |- ( ph -> A. z e. A A. y e. On ( z e. y \/ z = y \/ y e. z ) )   =>    |- ( ph -> ( A e. B \/ A = B \/ B e. A ) )
Theorem	exmidontriim 7571*	Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
|- (EXMID -> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
2.6.48  Excluded middle and the power set of a singleton
Theorem	iftrueb01 7572	Using an if expression to represent a truth value by (/) or 1o. Unlike some theorems using if, ph does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
|- ( if ( ph , 1o , (/) ) = 1o <-> ph )
Theorem	pw1m 7573*	A truth value which is inhabited is equal to true. This is a variation of pwntru 4331 and pwtrufal 16941. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
Theorem	pw1if 7574	Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( A e. ~P 1o -> if ( A = 1o , 1o , (/) ) = A )
Theorem	pw1on 7575	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
Theorem	pw1dom2 7576	The power set of 1o dominates 2o. Also see pwpw0ss 3925 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
|- 2o ~<_ ~P 1o
Theorem	pw1ne0 7577	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
Theorem	pw1ne1 7578	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
Theorem	pw1ne3 7579	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
Theorem	pw1nel3 7580	Negated excluded middle implies that the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> -. ~P 1o e. 3o )
Theorem	sucpw1ne3 7581	Negated excluded middle implies that the successor of the power set of 1o is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ( -. EXMID -> suc ~P 1o =/= 3o )
Theorem	sucpw1nel3 7582	The successor of the power set of 1o is not an element of 3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. suc ~P 1o e. 3o
Theorem	3nelsucpw1 7583	Three is not an element of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- -. 3o e. suc ~P 1o
Theorem	sucpw1nss3 7584	Negated excluded middle implies that the successor of the power set of 1o is not a subset of 3o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. suc ~P 1o C_ 3o )
Theorem	3nsssucpw1 7585	Negated excluded middle implies that 3o is not a subset of the successor of the power set of 1o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
|- ( -. EXMID -> -. 3o C_ suc ~P 1o )
Theorem	onntri35 7586*	Double negated ordinal trichotomy. There are five equivalent statements: (1) -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ), (2) -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ), (3) A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ), (4) A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ), and (5) -. -. EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7587), (3) implies (5) (onntri35 7586), (5) implies (1) (onntri51 7589), (2) implies (4) (onntri24 7591), (4) implies (5) (onntri45 7590), and (5) implies (2) (onntri52 7593). Another way of stating this is that EXMID is equivalent to trichotomy, either the x e. y \/ x = y \/ y e. x or the x C_ y \/ y C_ x form, as shown in exmidontri 7588 and exmidontri2or 7592, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7594 and (4) by onntri2or 7595. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) -> -. -. EXMID )
Theorem	onntri13 7587	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) -> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
Theorem	exmidontri 7588*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri51 7589*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri45 7590*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) -> -. -. EXMID )
Theorem	onntri24 7591	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) -> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
Theorem	exmidontri2or 7592*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
|- (EXMID <-> A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
Theorem	onntri52 7593*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
|- ( -. -. EXMID -> -. -. A. x e. On A. y e. On ( x C_ y \/ y C_ x ) )
Theorem	onntri3or 7594*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x e. y \/ x = y \/ y e. x ) )
Theorem	onntri2or 7595*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
|- ( -. -. EXMID <-> A. x e. On A. y e. On -. -. ( x C_ y \/ y C_ x ) )
Theorem	fmelpw1o 7596	With a formula ph one can associate an element of ~P 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than T. and F., by nndc 863, which translate to 1o and (/) respectively by iftrue 3642 and iffalse 3645, giving pwtrufal 16941). As proved in if0ab 3638, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.) (Proof shortened by BJ, 5-May-2026.)
|- if ( ph , 1o , (/) ) e. ~P 1o
2.6.49  Apartness relations
Syntax	wap 7597	Apartness predicate symbol.
wff R Ap A
Definition	df-pap 7598*	Apartness predicate. A relation R is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- ( R Ap A <-> ( ( R C_ ( A X. A ) /\ A. x e. A -. x R x ) /\ ( A. x e. A A. y e. A ( x R y -> y R x ) /\ A. x e. A A. y e. A A. z e. A ( x R y -> ( x R z \/ y R z ) ) ) ) )
Theorem	papeq1 7599	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( R = S -> ( R Ap A <-> S Ap A ) )
Theorem	papeq2 7600	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( A = B -> ( R Ap A <-> R Ap B ) )