P. 74 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7301-7400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cardonle 7301	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.)
⊢ (𝐴 ∈ On → (card‘𝐴) ⊆ 𝐴)
Theorem	card0 7302	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	ficardon 7303	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ On)
Theorem	carden2bex 7304*	If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵))
Theorem	pm54.43 7305	Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	pr2nelem 7306	Lemma for pr2ne 7307. (Contributed by FL, 17-Aug-2008.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 7307	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	exmidonfinlem 7308*	Lemma for exmidonfin 7309. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}    ⇒   ⊢ (ω = (On ∩ Fin) → DECID 𝜑)
Theorem	exmidonfin 7309	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 6976 and nnon 4662. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ (ω = (On ∩ Fin) → EXMID)
Theorem	en2eleq 7310	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.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})})
Theorem	en2other2 7311	Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋)
Theorem	dju1p1e2 7312	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	infpwfidom 7313	The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin))
Theorem	exmidfodomrlemeldju 7314	Lemma for exmidfodomr 7319. A variant of djur 7178. (Contributed by Jim Kingdon, 2-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))
Theorem	exmidfodomrlemreseldju 7315	Lemma for exmidfodomrlemrALT 7318. A variant of eldju 7177. (Contributed by Jim Kingdon, 9-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅)))
Theorem	exmidfodomrlemim 7316*	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 → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
Theorem	exmidfodomrlemr 7317*	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.)
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)
Theorem	exmidfodomrlemrALT 7318*	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 7317. In particular, this proof uses eldju 7177 instead of djur 7178 and avoids djulclb 7164. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)
Theorem	exmidfodomr 7319*	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 ↔ ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦))
Theorem	acnrcl 7320	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V)
Theorem	acneq 7321	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶)
Theorem	isacnm 7322*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑋 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)))
Theorem	finacn 7323	Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → AC 𝐴 = V)
2.6.42  Axiom of Choice equivalents
Syntax	wac 7324	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7325*	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 4589 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 ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))
Theorem	acfun 7326*	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.)
⊢ (𝜑 → CHOICE)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥))
Theorem	exmidaclem 7327*	Lemma for exmidac 7328. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (CHOICE → EXMID)
Theorem	exmidac 7328	The axiom of choice implies excluded middle. See acexmid 5950 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 7329	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	djuen 7330	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷))
Theorem	djuenun 7331	Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ∪ 𝐷))
Theorem	dju1en 7332	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 ⊔ 1o) ≈ suc 𝐴)
Theorem	dju0en 7333	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.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊔ ∅) ≈ 𝐴)
Theorem	xp2dju 7334	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 × 𝐴) = (𝐴 ⊔ 𝐴)
Theorem	djucomen 7335	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴))
Theorem	djuassen 7336	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵 ⊔ 𝐶)))
Theorem	xpdjuen 7337	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 ⊔ 𝐶)) ≈ ((𝐴 × 𝐵) ⊔ (𝐴 × 𝐶)))
Theorem	djudoml 7338	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵))
Theorem	djudomr 7339	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≼ (𝐴 ⊔ 𝐵))
2.6.44  Ordinal trichotomy
Theorem	exmidontriimlem1 7340	Lemma for exmidontriim 7344. A variation of r19.30dc 2654. (Contributed by Jim Kingdon, 12-Aug-2024.)
⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) → (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	exmidontriimlem2 7341*	Lemma for exmidontriim 7344. (Contributed by Jim Kingdon, 12-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ ∀𝑦 ∈ 𝐵 𝑦 ∈ 𝐴))
Theorem	exmidontriimlem3 7342*	Lemma for exmidontriim 7344. What we get to do based on induction on both 𝐴 and 𝐵. (Contributed by Jim Kingdon, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	exmidontriimlem4 7343*	Lemma for exmidontriim 7344. The induction step for the induction on 𝐴. (Contributed by Jim Kingdon, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	exmidontriim 7344*	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 → ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
2.6.45  Excluded middle and the power set of a singleton
Theorem	pw1on 7345	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
⊢ 𝒫 1o ∈ On
Theorem	pw1dom2 7346	The power set of 1o dominates 2o. Also see pwpw0ss 3847 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
⊢ 2o ≼ 𝒫 1o
Theorem	pw1ne0 7347	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ ∅
Theorem	pw1ne1 7348	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ 1o
Theorem	pw1ne3 7349	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ 3o
Theorem	pw1nel3 7350	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 → ¬ 𝒫 1o ∈ 3o)
Theorem	sucpw1ne3 7351	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 𝒫 1o ≠ 3o)
Theorem	sucpw1nel3 7352	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 𝒫 1o ∈ 3o
Theorem	3nelsucpw1 7353	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 ∈ suc 𝒫 1o
Theorem	sucpw1nss3 7354	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 𝒫 1o ⊆ 3o)
Theorem	3nsssucpw1 7355	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 ⊆ suc 𝒫 1o)
Theorem	onntri35 7356*	Double negated ordinal trichotomy. There are five equivalent statements: (1) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (2) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), (3) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (4) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), and (5) ¬ ¬ EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7357), (3) implies (5) (onntri35 7356), (5) implies (1) (onntri51 7359), (2) implies (4) (onntri24 7361), (4) implies (5) (onntri45 7360), and (5) implies (2) (onntri52 7363). Another way of stating this is that EXMID is equivalent to trichotomy, either the 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 or the 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 form, as shown in exmidontri 7358 and exmidontri2or 7362, respectively. Thus ¬ ¬ EXMID is equivalent to (1) or (2). In addition, ¬ ¬ EXMID is equivalent to (3) by onntri3or 7364 and (4) by onntri2or 7365. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ EXMID)
Theorem	onntri13 7357	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	exmidontri 7358*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
⊢ (EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	onntri51 7359*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	onntri45 7360*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ¬ ¬ EXMID)
Theorem	onntri24 7361	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
Theorem	exmidontri2or 7362*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
⊢ (EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
Theorem	onntri52 7363*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
Theorem	onntri3or 7364*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
⊢ (¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	onntri2or 7365*	Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
⊢ (¬ ¬ EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥))
2.6.46  Apartness relations
Syntax	wap 7366	Apartness predicate symbol.
wff 𝑅 Ap 𝐴
Definition	df-pap 7367*	Apartness predicate. A relation 𝑅 is an apartness if it is irreflexive, symmetric, and cotransitive. (Contributed by Jim Kingdon, 14-Feb-2025.)
⊢ (𝑅 Ap 𝐴 ↔ ((𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)))))
Syntax	wtap 7368	Tight apartness predicate symbol.
wff 𝑅 TAp 𝐴
Definition	df-tap 7369*	Tight apartness predicate. A relation 𝑅 is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.)
⊢ (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))
Theorem	dftap2 7370*	Tight apartness with the apartness properties from df-pap 7367 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.)
⊢ (𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))))
Theorem	tapeq1 7371	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.)
⊢ (𝑅 = 𝑆 → (𝑅 TAp 𝐴 ↔ 𝑆 TAp 𝐴))
Theorem	tapeq2 7372	Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.)
⊢ (𝐴 = 𝐵 → (𝑅 TAp 𝐴 ↔ 𝑅 TAp 𝐵))
Theorem	netap 7373*	Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴)
Theorem	2onetap 7374*	Negated equality is a tight apartness on 2o. (Contributed by Jim Kingdon, 6-Feb-2025.)
⊢ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ 𝑢 ≠ 𝑣)} TAp 2o
Theorem	2oneel 7375*	∅ and 1o are two unequal elements of 2o. (Contributed by Jim Kingdon, 8-Feb-2025.)
⊢ ⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ 𝑢 ≠ 𝑣)}
Theorem	2omotaplemap 7376*	Lemma for 2omotap 7378. (Contributed by Jim Kingdon, 6-Feb-2025.)
⊢ (¬ ¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o)
Theorem	2omotaplemst 7377*	Lemma for 2omotap 7378. (Contributed by Jim Kingdon, 6-Feb-2025.)
⊢ ((∃*𝑟 𝑟 TAp 2o ∧ ¬ ¬ 𝜑) → 𝜑)
Theorem	2omotap 7378	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.)
⊢ (∃*𝑟 𝑟 TAp 2o → EXMID)
Theorem	exmidapne 7379*	Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.)
⊢ (EXMID → (𝑅 TAp 𝐴 ↔ 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}))
Theorem	exmidmotap 7380*	The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.)
⊢ (EXMID ↔ ∀𝑥∃*𝑟 𝑟 TAp 𝑥)
PART 3  CHOICE PRINCIPLES We have already introduced the full Axiom of Choice df-ac 7325 but since it implies excluded middle as shown at exmidac 7328, 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 7381	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7382*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7325 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
⊢ (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)))
Theorem	ccfunen 7383*	Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → 𝐴 ≈ ω)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥))
Theorem	cc1 7384*	Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
⊢ (CCHOICE → ∀𝑥((𝑥 ≈ ω ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 𝑤 ∈ 𝑧) → ∃𝑓∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ∈ 𝑧))
Theorem	cc2lem 7385*	Lemma for cc2 7386. (Contributed by Jim Kingdon, 27-Apr-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → 𝐹 Fn ω)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))    &   ⊢ 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴‘𝑛))))    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
Theorem	cc2 7386*	Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → 𝐹 Fn ω)    &   ⊢ (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔‘𝑛) ∈ (𝐹‘𝑛)))
Theorem	cc3 7387*	Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 𝐹 ∈ V)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ 𝐹)    &   ⊢ (𝜑 → 𝑁 ≈ ω)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐹))
Theorem	cc4f 7388*	Countable choice by showing the existence of a function 𝑓 which can choose a value at each index 𝑛 such that 𝜒 holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ Ⅎ𝑛𝐴    &   ⊢ (𝜑 → 𝑁 ≈ ω)    &   ⊢ (𝑥 = (𝑓‘𝑛) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜒))
Theorem	cc4 7389*	Countable choice by showing the existence of a function 𝑓 which can choose a value at each index 𝑛 such that 𝜒 holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ≈ ω)    &   ⊢ (𝑥 = (𝑓‘𝑛) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜒))
Theorem	cc4n 7390*	Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7389, the hypotheses only require an A(n) for each value of 𝑛, not a single set 𝐴 which suffices for every 𝑛 ∈ ω. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
⊢ (𝜑 → CCHOICE)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ≈ ω)    &   ⊢ (𝑥 = (𝑓‘𝑛) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒))
Theorem	acnccim 7391	Given countable choice, every set has choice sets of length ω. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (CCHOICE → AC ω = 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 6567 and similar theorems ), going from there to positive integers (df-ni 7424) and then positive rational numbers (df-nqqs 7468) 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 7586. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 8052 and the MacNeille reals fail to satisfy axltwlin 8147, 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 7392	The set of positive integers, which is the set of natural numbers ω with 0 removed. Note: This is the start of the Dedekind-cut construction of real and complex numbers.
class N
Syntax	cpli 7393	Positive integer addition.
class +N
Syntax	cmi 7394	Positive integer multiplication.
class ·N
Syntax	clti 7395	Positive integer ordering relation.
class <N
Syntax	cplpq 7396	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 7397	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 7398	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 7399	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 7400	Set of positive fractions.
class Q