P. 75 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exmidfodomrlemreseldju 7401	Lemma for exmidfodomrlemrALT 7404. A variant of eldju 7258. (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 7402*	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 7403*	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 7404*	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 7403. In particular, this proof uses eldju 7258 instead of djur 7259 and avoids djulclb 7245. (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 7405*	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 7406	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( X e. AC A -> A e. _V )
Theorem	acneq 7407	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A = C -> AC A = AC C )
Theorem	isacnm 7408*	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 7409	Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- ( A e. Fin -> AC A = _V )
2.6.42  Axiom of Choice equivalents
Syntax	wac 7410	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7411*	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 4633 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 7412*	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 7413*	Lemma for exmidac 7414. 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 7414	The axiom of choice implies excluded middle. See acexmid 6012 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.43  Cardinal number arithmetic
Theorem	endjudisj 7415	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 7416	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7417	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 7418	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 7419	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 7420	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 7421	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 7422	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 7423	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 7424	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 7425	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.44  Ordinal trichotomy
Theorem	exmidontriimlem1 7426	Lemma for exmidontriim 7430. A variation of r19.30dc 2678. (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 7427*	Lemma for exmidontriim 7430. (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 7428*	Lemma for exmidontriim 7430. 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 7429*	Lemma for exmidontriim 7430. 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 7430*	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.45  Excluded middle and the power set of a singleton
Theorem	iftrueb01 7431	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 7432*	A truth value which is inhabited is equal to true. This is a variation of pwntru 4287 and pwtrufal 16534. (Contributed by Jim Kingdon, 10-Jan-2026.)
|- ( ( A e. ~P 1o /\ E. x x e. A ) -> A = 1o )
Theorem	pw1if 7433	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 7434	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
|- ~P 1o e. On
Theorem	pw1dom2 7435	The power set of 1o dominates 2o. Also see pwpw0ss 3886 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
|- 2o ~<_ ~P 1o
Theorem	pw1ne0 7436	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= (/)
Theorem	pw1ne1 7437	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 1o
Theorem	pw1ne3 7438	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
|- ~P 1o =/= 3o
Theorem	pw1nel3 7439	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 7440	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 7441	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 7442	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 7443	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 7444	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 7445*	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 7446), (3) implies (5) (onntri35 7445), (5) implies (1) (onntri51 7448), (2) implies (4) (onntri24 7450), (4) implies (5) (onntri45 7449), and (5) implies (2) (onntri52 7452). 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 7447 and exmidontri2or 7451, respectively. Thus -. -. EXMID is equivalent to (1) or (2). In addition, -. -. EXMID is equivalent to (3) by onntri3or 7453 and (4) by onntri2or 7454. (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 7446	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 7447*	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 7448*	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 7449*	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 7450	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 7451*	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 7452*	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 7453*	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 7454*	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 7455	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 856, which translate to 1o and (/) respectively by iftrue 3608 and iffalse 3611, giving pwtrufal 16534). As proved in if0ab 16337, the associated element of ~P 1o is the extension, in ~P 1o, of the formula ph. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , 1o , (/) ) e. ~P 1o
2.6.46  Apartness relations
Syntax	wap 7456	Apartness predicate symbol.
wff R Ap A
Definition	df-pap 7457*	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 ) ) ) ) )
Syntax	wtap 7458	Tight apartness predicate symbol.
wff R TAp A
Definition	df-tap 7459*	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	dftap2 7460*	Tight apartness with the apartness properties from df-pap 7457 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 7461	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
|- ( R = S -> ( R TAp A <-> S TAp A ) )
Theorem	tapeq2 7462	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
|- ( A = B -> ( R TAp A <-> R TAp B ) )
Theorem	netap 7463*	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 7464*	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 7465*	(/) 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 7466*	Lemma for 2omotap 7468. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( -. -. ph -> { <. u , v >. | ( ( u e. 2o /\ v e. 2o ) /\ ( ph /\ u =/= v ) ) } TAp 2o )
Theorem	2omotaplemst 7467*	Lemma for 2omotap 7468. (Contributed by Jim Kingdon, 6-Feb-2025.)
|- ( ( E* r r TAp 2o /\ -. -. ph ) -> ph )
Theorem	2omotap 7468	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 7469*	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 7470*	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 7411 but since it implies excluded middle as shown at exmidac 7414, 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 7471	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7472*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7411 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 7473*	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 7474*	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 7475*	Lemma for cc2 7476. (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 7476*	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 7477*	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 7478*	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 7479*	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 ) )
Theorem	cc4n 7480*	Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7479, the hypotheses only require an A(n) for each value of n, not a single set A which suffices for every n e. om. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A. n e. N { x e. A | ps } e. V )   &    |- ( ph -> N ~~ om )   &    |- ( x = ( f ` n ) -> ( ps <-> ch ) )   &    |- ( ph -> A. n e. N E. x e. A ps )   =>    |- ( ph -> E. f ( f Fn N /\ A. n e. N ch ) )
Theorem	acnccim 7481	Given countable choice, every set has choice sets of length om. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- (CCHOICE -> AC om = _V )
PART 4  REAL AND COMPLEX NUMBERS This section derives the basics of real and complex numbers. To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6637 and similar theorems ), going from there to positive integers (df-ni 7514) and then positive rational numbers (df-nqqs 7558) does not involve a major change in approach compared with the Metamath Proof Explorer. It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle or choice principles. With excluded middle, it is natural to define a cut as the lower set only (as Metamath Proof Explorer does), but here we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero". When working constructively, there are several possible definitions of real numbers. Here we adopt the most common definition, as two-sided Dedekind cuts with the properties described at df-inp 7676. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 8142 and the MacNeille reals fail to satisfy axltwlin 8237, and we do not develop them here. For more on differing definitions of the reals, see the introduction to Chapter 11 in [HoTT] or Section 1.2 of [BauerHanson].
4.1  Construction and axiomatization of real and complex numbers
4.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 7482	The set of positive integers, which is the set of natural numbers om with 0 removed. Note: This is the start of the Dedekind-cut construction of real and complex numbers.
class N.
Syntax	cpli 7483	Positive integer addition.
class +N
Syntax	cmi 7484	Positive integer multiplication.
class .N
Syntax	clti 7485	Positive integer ordering relation.
class <N
Syntax	cplpq 7486	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 7487	Positive pre-fraction multiplication.
class .pQ
Syntax	cltpq 7488	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 7489	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 7490	Set of positive fractions.
class Q.
Syntax	c1q 7491	The positive fraction constant 1.
class 1Q
Syntax	cplq 7492	Positive fraction addition.
class +Q
Syntax	cmq 7493	Positive fraction multiplication.
class .Q
Syntax	crq 7494	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 7495	Positive fraction ordering relation.
class <Q
Syntax	ceq0 7496	Equivalence class used to construct nonnegative fractions.
class ~Q0
Syntax	cnq0 7497	Set of nonnegative fractions.
class Q0
Syntax	c0q0 7498	The nonnegative fraction constant 0.
class 0Q0
Syntax	cplq0 7499	Nonnegative fraction addition.
class +Q0
Syntax	cmq0 7500	Nonnegative fraction multiplication.
class ·Q0