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	pr2nelem 7501	Lemma for pr2ne 7502. (Contributed by FL, 17-Aug-2008.)
|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )
Theorem	pr2ne 7502	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 7503*	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 7504	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 7505	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 7506	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 7507	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 7508*	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 7509*	Lemma for exmidonfin 7510. (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 7510	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 7140 and nnon 4737. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- ( om = ( On i^i Fin ) -> EXMID )
Theorem	en2eleq 7511	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 7512	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 7513	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( 1o ⊔ 1o ) ~~ 2o
Theorem	infpwfidom 7514	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 7515	Lemma for exmidfodomr 7520. A variant of djur 7373. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( ph -> A C_ 1o )   &    |- ( ph -> B e. ( A ⊔ 1o ) )   =>    |- ( ph -> ( B = (inl ` (/) ) \/ B = (inr ` (/) ) ) )
Theorem	exmidfodomrlemreseldju 7516	Lemma for exmidfodomrlemrALT 7519. A variant of eldju 7372. (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 7517*	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 7518*	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 7519*	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 7518. In particular, this proof uses eldju 7372 instead of djur 7373 and avoids djulclb 7359. (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 7520*	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 7521	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( X e. AC A -> A e. _V )
Theorem	acneq 7522	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A = C -> AC A = AC C )
Theorem	isacnm 7523*	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 7524	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 7525	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7526*	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 4664 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 7527*	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 7528*	Lemma for exmidac 7529. 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 7529	The axiom of choice implies excluded middle. See acexmid 6057 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 7530	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 7531	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7532	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 7533	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 7534	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 7535	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 7536	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 7537	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 7538	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 7539	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 7540	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 7541	Lemma for exmidontriim 7545. A variation of r19.30dc 2692. (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 7542*	Lemma for exmidontriim 7545. (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 7543*	Lemma for exmidontriim 7545. 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 7544*	Lemma for exmidontriim 7545. 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 7545*	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 7546	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 7547*	A truth value which is inhabited is equal to true. This is a variation of pwntru 4317 and pwtrufal 16897. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
Theorem	pw1if 7548	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 7549	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
Theorem	pw1dom2 7550	The power set of 1o dominates 2o. Also see pwpw0ss 3914 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
|- 2o ~<_ ~P 1o
Theorem	pw1ne0 7551	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
Theorem	pw1ne1 7552	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
Theorem	pw1ne3 7553	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
Theorem	pw1nel3 7554	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 7555	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 7556	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 7557	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 7558	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 7559	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 7560*	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 7561), (3) implies (5) (onntri35 7560), (5) implies (1) (onntri51 7563), (2) implies (4) (onntri24 7565), (4) implies (5) (onntri45 7564), and (5) implies (2) (onntri52 7567). 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 7562 and exmidontri2or 7566, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7568 and (4) by onntri2or 7569. (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 7561	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 7562*	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 7563*	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 7564*	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 7565	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 7566*	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 7567*	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 7568*	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 7569*	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 7570	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 859, which translate to 1o and (/) respectively by iftrue 3631 and iffalse 3634, giving pwtrufal 16897). As proved in if0ab 3627, 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 7571	Apartness predicate symbol.
wff R Ap A
Definition	df-pap 7572*	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 7573	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( R = S -> ( R Ap A <-> S Ap A ) )
Theorem	papeq2 7574	Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
|- ( A = B -> ( R Ap A <-> R Ap B ) )
Theorem	papirr 7575	An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ( R Ap A /\ X e. A ) -> -. X R X )
Theorem	papsym 7576	An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.)
|- ( ph -> R Ap A )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> X R Y )   =>    |- ( ph -> Y R X )
Theorem	papcotr 7577	An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.)
|- ( ph -> R Ap A )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- ( ph -> X R Y )   &    |- ( ph -> Z e. A )   =>    |- ( ph -> ( X R Z \/ Y R Z ) )
Syntax	wtap 7578	Tight apartness predicate symbol.
wff R TAp A
Definition	df-tap 7579*	Tight apartness predicate. A relation R is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
|- ( R TAp A <-> ( R Ap A /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) )
Theorem	tapap 7580	A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.)
|- ( R TAp A -> R Ap A )
Theorem	dftap2 7581*	Tight apartness with the apartness properties from df-pap 7572 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
|- ( R TAp 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 ) ) /\ A. x e. A A. y e. A ( -. x R y -> x = y ) ) ) )
Theorem	tapeq1 7582	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- ( R = S -> ( R TAp A <-> S TAp A ) )
Theorem	tapeq2 7583	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
|- ( A = B -> ( R TAp A <-> R TAp B ) )
Theorem	netap 7584*	Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
|- ( A. x e. A A. y e. A DECID x = y -> { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } TAp A )
Theorem	2onetap 7585*	Negated equality is a tight apartness on 2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ u =/= v ) } TAp 2o
Theorem	2oneel 7586*	(/) and 1o are two unequal elements of 2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- <. (/) , 1o >. e. { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ u =/= v ) }
Theorem	2omotaplemap 7587*	Lemma for 2omotap 7589. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( -. -. ph -> { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ ( ph /\ u =/= v ) ) } TAp 2o )
Theorem	2omotaplemst 7588*	Lemma for 2omotap 7589. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( ( E* r r TAp 2o /\ -. -. ph ) -> ph )
Theorem	2omotap 7589	If there is at most one tight apartness on 2o, excluded middle follows. Based on online discussions by Tom de Jong, Andrew W Swan, and Martin Escardo. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( E* r r TAp 2o -> EXMID )
Theorem	exmidapne 7590*	Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- (EXMID -> ( R TAp A <-> R = { <. u , v >. | ( ( u e. A /\ v e. A ) /\ u =/= v ) } ) )
Theorem	exmidmotap 7591*	The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
|- (EXMID <-> A. x E* r r TAp x )
PART 3  CHOICE PRINCIPLES We have already introduced the full Axiom of Choice df-ac 7526 but since it implies excluded middle as shown at exmidac 7529, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.
3.1  Countable Choice and Dependent Choice
3.1.1  Introduce Countable Choice
Syntax	wacc 7592	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7593*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7526 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
Theorem	ccfunen 7594*	Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A ~~ om )   &    |- ( 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	cc1 7595*	Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- (CCHOICE -> A. x ( ( x ~~ om /\ A. z e. x E. w w e. z ) -> E. f A. z e. x ( f ` z ) e. z ) )
Theorem	cc2lem 7596*	Lemma for cc2 7597. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   &    |- A = ( n e. om |-> ( { n } X. ( F ` n ) ) )   &    |- G = ( n e. om |-> ( 2nd ` ( f ` ( A ` n ) ) ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc2 7597*	Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc3 7598*	Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A. n e. N F e. _V )   &    |- ( ph -> A. n e. N E. w w e. F )   &    |- ( ph -> N ~~ om )   =>    |- ( ph -> E. f ( f Fn N /\ A. n e. N ( f ` n ) e. F ) )
Theorem	cc4f 7599*	Countable choice by showing the existence of a function f which can choose a value at each index n such that ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A e. V )   &    |- F/_ n A   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f : N --> A /\ A. n e. N ch ) )
Theorem	cc4 7600*	Countable choice by showing the existence of a function f which can choose a value at each index n such that ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A e. V )   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f : N --> A /\ A. n e. N ch ) )