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	enmkvlem 7501	Lemma for enmkv 7502. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov → 𝐵 ∈ Markov))
Theorem	enmkv 7502	Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either ω ∈ Markov or ℕ0 ∈ Markov. The former is a better match to conventional notation in the sense that df2o3 6702 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 24-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ Markov ↔ 𝐵 ∈ Markov))
2.6.43  Weakly omniscient sets
Syntax	cwomni 7503	Extend class definition to include the class of weakly omniscient sets.
class WOmni
Definition	df-womni 7504*	A weakly omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1o) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, ω ∈ WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → DECID ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)}
Theorem	iswomni 7505*	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓(𝑓:𝐴⟶2o → DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))
Theorem	iswomnimap 7506*	The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ (2o ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))
Theorem	omniwomnimkv 7507	A set is omniscient if and only if it is weakly omniscient and Markov. The case 𝐴 = ω says that LPO ↔ WLPO ∧ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
⊢ (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov))
Theorem	lpowlpo 7508	LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7507. There is an analogue in terms of analytic omniscience principles at tridceq 17118. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (ω ∈ Omni → ω ∈ WOmni)
Theorem	enwomnilem 7509	Lemma for enwomni 7510. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni → 𝐵 ∈ WOmni))
Theorem	enwomni 7510	Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either ω ∈ WOmni or ℕ0 ∈ WOmni. The former is a better match to conventional notation in the sense that df2o3 6702 says that 2o = {∅, 1o} whereas the corresponding relationship does not exist between 2 and {0, 1}. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ WOmni ↔ 𝐵 ∈ WOmni))
Theorem	nninfdcinf 7511*	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.)
⊢ (𝜑 → ω ∈ WOmni)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ∞)    ⇒   ⊢ (𝜑 → DECID 𝑁 = (𝑖 ∈ ω ↦ 1o))
Theorem	nninfwlporlemd 7512*	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.)
⊢ (𝜑 → 𝑋:ω⟶2o)    &   ⊢ (𝜑 → 𝑌:ω⟶2o)    &   ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    ⇒   ⊢ (𝜑 → (𝑋 = 𝑌 ↔ 𝐷 = (𝑖 ∈ ω ↦ 1o)))
Theorem	nninfwlporlem 7513*	Lemma for nninfwlpor 7514. The result. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (𝜑 → 𝑋:ω⟶2o)    &   ⊢ (𝜑 → 𝑌:ω⟶2o)    &   ⊢ 𝐷 = (𝑖 ∈ ω ↦ if((𝑋‘𝑖) = (𝑌‘𝑖), 1o, ∅))    &   ⊢ (𝜑 → ω ∈ WOmni)    ⇒   ⊢ (𝜑 → DECID 𝑋 = 𝑌)
Theorem	nninfwlpor 7514*	The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.)
⊢ (ω ∈ WOmni → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)
Theorem	nninfwlpoimlemg 7515*	Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ℕ∞)
Theorem	nninfwlpoimlemginf 7516*	Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    ⇒   ⊢ (𝜑 → (𝐺 = (𝑖 ∈ ω ↦ 1o) ↔ ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o))
Theorem	nninfwlpoimlemdc 7517*	Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)
Theorem	nninfinfwlpolem 7518*	Lemma for nninfinfwlpo 7520. (Contributed by Jim Kingdon, 8-Dec-2024.)
⊢ (𝜑 → 𝐹:ω⟶2o)    &   ⊢ 𝐺 = (𝑖 ∈ ω ↦ if(∃𝑥 ∈ suc 𝑖(𝐹‘𝑥) = ∅, ∅, 1o))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ∞ DECID 𝑥 = (𝑖 ∈ ω ↦ 1o))    ⇒   ⊢ (𝜑 → DECID ∀𝑛 ∈ ω (𝐹‘𝑛) = 1o)
Theorem	nninfwlpoim 7519*	Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.)
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
Theorem	nninfinfwlpo 7520*	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 7473). (Contributed by Jim Kingdon, 25-Nov-2025.)
⊢ (∀𝑥 ∈ ℕ∞ DECID 𝑥 = (𝑖 ∈ ω ↦ 1o) ↔ ω ∈ WOmni)
Theorem	nninfwlpo 7521*	Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.)
⊢ (∀𝑥 ∈ ℕ∞ ∀𝑦 ∈ ℕ∞ DECID 𝑥 = 𝑦 ↔ ω ∈ WOmni)
2.6.44  Cardinal numbers
Syntax	ccrd 7522	Extend class definition to include the cardinal size function.
class card
Syntax	wacn 7523	The axiom of choice for limited-length sequences.
class AC 𝐴
Definition	df-card 7524*	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 = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥})
Definition	df-acnm 7525*	Define a local and length-limited version of the axiom of choice. The definition of the predicate 𝑋 ∈ AC 𝐴 is that for all families of inhabited subsets of 𝑋 indexed on 𝐴 (i.e. functions 𝐴⟶{𝑧 ∈ 𝒫 𝑋 ∣ ∃𝑗𝑗 ∈ 𝑧}), 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 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
Theorem	cardcl 7526*	The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ (∃𝑦 ∈ On 𝑦 ≈ 𝐴 → (card‘𝐴) ∈ On)
Theorem	isnumi 7527	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card)
Theorem	finnum 7528	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
Theorem	onenon 7529	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)
Theorem	cardval3ex 7530*	The value of (card‘𝐴). (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ (∃𝑥 ∈ On 𝑥 ≈ 𝐴 → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
Theorem	oncardval 7531*	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.)
⊢ (𝐴 ∈ On → (card‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝑥 ≈ 𝐴})
Theorem	cardonle 7532	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 7533	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	ficardon 7534	The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ On)
Theorem	carden2bex 7535*	If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
⊢ ((𝐴 ≈ 𝐵 ∧ ∃𝑥 ∈ On 𝑥 ≈ 𝐴) → (card‘𝐴) = (card‘𝐵))
Theorem	pm54.43 7536	Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	pr2nelem 7537	Lemma for pr2ne 7538. (Contributed by FL, 17-Aug-2008.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 7538	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	en2prde 7539*	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.)
⊢ (𝑉 ≈ 2o → ∃𝑎∃𝑏(𝑎 ≠ 𝑏 ∧ 𝑉 = {𝑎, 𝑏}))
Theorem	pr1or2 7540	An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ DECID 𝐴 = 𝐵) → ({𝐴, 𝐵} ≈ 1o ∨ {𝐴, 𝐵} ≈ 2o))
Theorem	pr2cv1 7541	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V)
Theorem	pr2cv2 7542	If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V)
Theorem	pr2cv 7543	If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.)
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	sspw1or2 7544*	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.)
⊢ {𝑥 ∈ {𝑠 ∈ 𝒫 𝑉 ∣ ∃𝑗 𝑗 ∈ 𝑠} ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)} = {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}
Theorem	exmidonfinlem 7545*	Lemma for exmidonfin 7546. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ 𝐴 = {{𝑥 ∈ {∅} ∣ 𝜑}, {𝑥 ∈ {∅} ∣ ¬ 𝜑}}    ⇒   ⊢ (ω = (On ∩ Fin) → DECID 𝜑)
Theorem	exmidonfin 7546	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 7174 and nnon 4757. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
⊢ (ω = (On ∩ Fin) → EXMID)
Theorem	en2eleq 7547	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 7548	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 7549	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
⊢ (1o ⊔ 1o) ≈ 2o
Theorem	infpwfidom 7550	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 7551	Lemma for exmidfodomr 7556. A variant of djur 7409. (Contributed by Jim Kingdon, 2-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅)))
Theorem	exmidfodomrlemreseldju 7552	Lemma for exmidfodomrlemrALT 7555. A variant of eldju 7408. (Contributed by Jim Kingdon, 9-Jul-2022.)
⊢ (𝜑 → 𝐴 ⊆ 1o)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1o))    ⇒   ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1o)‘∅)))
Theorem	exmidfodomrlemim 7553*	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 7554*	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 7555*	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 7554. In particular, this proof uses eldju 7408 instead of djur 7409 and avoids djulclb 7395. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID)
Theorem	exmidfodomr 7556*	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 7557	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V)
Theorem	acneq 7558	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶)
Theorem	isacnm 7559*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑋 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)))
Theorem	finacn 7560	Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → AC 𝐴 = V)
2.6.45  Axiom of Choice equivalents
Syntax	wac 7561	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7562*	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 4684 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 7563*	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 7564*	Lemma for exmidac 7565. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})}    &   ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})}    &   ⊢ 𝐶 = {𝐴, 𝐵}    ⇒   ⊢ (CHOICE → EXMID)
Theorem	exmidac 7565	The axiom of choice implies excluded middle. See acexmid 6084 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 7566	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵))
Theorem	djuen 7567	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷))
Theorem	djuenun 7568	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 7569	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 7570	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 7571	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 7572	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 7573	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 7574	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 7575	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵))
Theorem	djudomr 7576	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≼ (𝐴 ⊔ 𝐵))
2.6.47  Ordinal trichotomy
Theorem	exmidontriimlem1 7577	Lemma for exmidontriim 7581. A variation of r19.30dc 2698. (Contributed by Jim Kingdon, 12-Aug-2024.)
⊢ ((∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) → (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	exmidontriimlem2 7578*	Lemma for exmidontriim 7581. (Contributed by Jim Kingdon, 12-Aug-2024.)
⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ ∀𝑦 ∈ 𝐵 𝑦 ∈ 𝐴))
Theorem	exmidontriimlem3 7579*	Lemma for exmidontriim 7581. What we get to do based on induction on both 𝐴 and 𝐵. (Contributed by Jim Kingdon, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    &   ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ∨ 𝑦 ∈ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	exmidontriimlem4 7580*	Lemma for exmidontriim 7581. The induction step for the induction on 𝐴. (Contributed by Jim Kingdon, 10-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → EXMID)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ On (𝑧 ∈ 𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦 ∈ 𝑧))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
Theorem	exmidontriim 7581*	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.48  Excluded middle and the power set of a singleton
Theorem	iftrueb01 7582	Using an if expression to represent a truth value by ∅ or 1o. Unlike some theorems using if, 𝜑 does not need to be decidable. (Contributed by Jim Kingdon, 9-Jan-2026.)
⊢ (if(𝜑, 1o, ∅) = 1o ↔ 𝜑)
Theorem	pw1m 7583*	A truth value which is inhabited is equal to true. This is a variation of pwntru 4336 and pwtrufal 17039. (Contributed by Jim Kingdon, 10-Jan-2026.)
⊢ ((𝐴 ∈ 𝒫 1o ∧ ∃𝑥 𝑥 ∈ 𝐴) → 𝐴 = 1o)
Theorem	pw1if 7584	Expressing a truth value in terms of an if expression. (Contributed by Jim Kingdon, 10-Jan-2026.)
⊢ (𝐴 ∈ 𝒫 1o → if(𝐴 = 1o, 1o, ∅) = 𝐴)
Theorem	pw1on 7585	The power set of 1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
⊢ 𝒫 1o ∈ On
Theorem	pw1dom2 7586	The power set of 1o dominates 2o. Also see pwpw0ss 3930 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.)
⊢ 2o ≼ 𝒫 1o
Theorem	pw1ne0 7587	The power set of 1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ ∅
Theorem	pw1ne1 7588	The power set of 1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ 1o
Theorem	pw1ne3 7589	The power set of 1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
⊢ 𝒫 1o ≠ 3o
Theorem	pw1nel3 7590	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 7591	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 7592	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 7593	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 7594	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 7595	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 7596*	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 7597), (3) implies (5) (onntri35 7596), (5) implies (1) (onntri51 7599), (2) implies (4) (onntri24 7601), (4) implies (5) (onntri45 7600), and (5) implies (2) (onntri52 7603). Another way of stating this is that EXMID is equivalent to trichotomy, either the 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 or the 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 form, as shown in exmidontri 7598 and exmidontri2or 7602, respectively. Thus ¬ ¬ EXMID is equivalent to (1) or (2). In addition, ¬ ¬ EXMID is equivalent to (3) by onntri3or 7604 and (4) by onntri2or 7605. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ EXMID)
Theorem	onntri13 7597	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	exmidontri 7598*	Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
⊢ (EXMID ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	onntri51 7599*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (¬ ¬ EXMID → ¬ ¬ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
Theorem	onntri45 7600*	Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ¬ ¬ EXMID)