P. 174 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 17301-17400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nninfomni 17301	ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.)
⊢ ℕ∞ ∈ Omni
Theorem	nninffeq 17302*	Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, ⊢ (𝜑 → ∀𝑛 ∈ suc ω...). (Contributed by Jim Kingdon, 4-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ∞⟶ℕ0)    &   ⊢ (𝜑 → 𝐺:ℕ∞⟶ℕ0)    &   ⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1o)) = (𝐺‘(𝑥 ∈ ω ↦ 1o)))    &   ⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	nnnninfen 17303	Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
⊢ (ω ≈ ℕ∞ ↔ ω ∈ Omni)
Theorem	nnnninfex 17304*	If an element of ℕ∞ has a value of zero somewhere, then it is the mapping of a natural number. (Contributed by Jim Kingdon, 4-Aug-2022.)
⊢ (𝜑 → 𝑃 ∈ ℕ∞)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → (𝑃‘𝑁) = ∅)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ω 𝑃 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))
Theorem	nninfnfiinf 17305*	An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
⊢ ((𝐴 ∈ ℕ∞ ∧ ¬ ∃𝑛 ∈ ω 𝐴 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → 𝐴 = (𝑖 ∈ ω ↦ 1o))
14.4.7  Schroeder-Bernstein Theorem
Theorem	exmidsbthrlem 17306*	Lemma for exmidsbthr 17307. (Contributed by Jim Kingdon, 11-Aug-2022.)
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))))    ⇒   ⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)
Theorem	exmidsbthr 17307*	The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.)
⊢ (∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦) → EXMID)
Theorem	exmidsbth 17308*	The Schroeder-Bernstein Theorem is equivalent to excluded middle. This is Metamath 100 proof #25. The forward direction (isbth 7291) is the proof of the Schroeder-Bernstein Theorem from the Metamath Proof Explorer database (in which excluded middle holds), but adapted to use EXMID as an antecedent rather than being unconditionally true, as in the non-intuitionistic proof at https://us.metamath.org/mpeuni/sbth.html 7291. The reverse direction (exmidsbthr 17307) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.)
⊢ (EXMID ↔ ∀𝑥∀𝑦((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑥) → 𝑥 ≈ 𝑦))
Theorem	sbthomlem 17309	Lemma for sbthom 17310. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.)
⊢ (𝜑 → ω ∈ Omni)    &   ⊢ (𝜑 → 𝑌 ⊆ {∅})    &   ⊢ (𝜑 → 𝐹:ω–1-1-onto→(𝑌 ⊔ ω))    ⇒   ⊢ (𝜑 → (𝑌 = ∅ ∨ 𝑌 = {∅}))
Theorem	sbthom 17310	Schroeder-Bernstein is not possible even for ω. We know by exmidsbth 17308 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ω? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.)
⊢ ((∀𝑥((𝑥 ≼ ω ∧ ω ≼ 𝑥) → 𝑥 ≈ ω) ∧ ω ∈ Omni) → EXMID)
14.4.8  Real and complex numbers
Theorem	qdencn 17311*	The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 11991 (and also would hold for ℝ × ℝ with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
⊢ 𝑄 = {𝑧 ∈ ℂ ∣ ((ℜ‘𝑧) ∈ ℚ ∧ (ℑ‘𝑧) ∈ ℚ)}    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ 𝑄 (abs‘(𝑥 − 𝐴)) < 𝐵)
Theorem	refeq 17312*	Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → 𝐺:ℝ⟶ℝ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑥 < 0 → (𝐹‘𝑥) = (𝐺‘𝑥)))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (0 < 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥)))    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	repiecelem 17313*	Lemma for repiecele0 17314, repiecege0 17315, and repiecef 17316. The function 𝐻 is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
⊢ (𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℝ) → (((𝐹‘inf({𝐴, 0}, ℝ, < )) + (𝐺‘sup({𝐴, 0}, ℝ, < ))) − (𝐹‘0)) ∈ ℝ)
Theorem	repiecele0 17314*	Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17316 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
⊢ (𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (𝐻‘𝐴) = (𝐹‘𝐴))
Theorem	repiecege0 17315*	Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17316 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
⊢ (𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐻‘𝐴) = (𝐺‘𝐴))
Theorem	repiecef 17316*	Piecewise definition on the reals yields a function. The function agrees with 𝐹 and 𝐺 on their respective parts of the real line; see repiecele0 17314 and repiecege0 17315. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 17315 (Contributed by Jim Kingdon, 27-Apr-2026.)
⊢ (𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   ⊢ (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   ⊢ (𝜑 → (𝐹‘0) = (𝐺‘0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ⊢ (𝜑 → 𝐻:ℝ⟶ℝ)
Theorem	triap 17317	Two ways of stating real number trichotomy. See also cndcap 17349 which is similar but for complex number apartness. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) ↔ DECID 𝐴 # 𝐵))
Theorem	isomninnlem 17318*	Lemma for isomninn 17319. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
Theorem	isomninn 17319*	Omniscience stated in terms of natural numbers. Similar to isomnimap 7484 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1o. (Contributed by Jim Kingdon, 30-Aug-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Omni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0 ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1)))
Theorem	cvgcmp2nlemabs 17320*	Lemma for cvgcmp2n 17321. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting (seq1( + , 𝐺)‘𝑁) as the sum of (seq1( + , 𝐺)‘𝑀) and a term which gets smaller as 𝑀 gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀))
Theorem	cvgcmp2n 17321*	A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (1 / (2↑𝑘)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
Theorem	iooref1o 17322	A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (1 / (1 + (exp‘𝑥))))    ⇒   ⊢ 𝐹:ℝ–1-1-onto→(0(,)1)
Theorem	iooreen 17323	An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
⊢ (0(,)1) ≈ ℝ
Theorem	rirrdisj 17324*	The rational and irrational numbers are disjoint. Here irrational means apart from any rational number. (Contributed by Jim Kingdon, 18-Sep-2026.)
⊢ (ℚ ∩ {𝑥 ∈ ℝ ∣ ∀𝑞 ∈ ℚ 𝑥 # 𝑞}) = ∅
14.4.9  Analytic omniscience principles Omniscience principles refer to several propositions, most of them weaker than full excluded middle, which do not follow from the axioms of IZF set theory. They are: (0) the Principle of Omniscience (PO), which is another name for excluded middle (see exmidomni 7489), (1) the Limited Principle of Omniscience (LPO) is ω ∈ Omni (see df-omni 7482), (2) the Weak Limited Principle of Omniscience (WLPO) is ω ∈ WOmni (see df-womni 7511), (3) Markov's Principle (MP) is ω ∈ Markov (see df-markov 7499), (4) the Lesser Limited Principle of Omniscience (LLPO) is not yet defined in iset.mm. They also have analytic counterparts each of which follows from the corresponding omniscience principle: (1) Analytic LPO is real number trichotomy, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) (see trilpo 17332), (2) Analytic WLPO is decidability of real number equality, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝDECID 𝑥 = 𝑦 (see redcwlpo 17345), (3) Analytic MP is ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≠ 𝑦 → 𝑥 # 𝑦) (see neapmkv 17358), (4) Analytic LLPO is real number dichotomy, ∀𝑥 ∈ ℝ∀𝑦 ∈ ℝ(𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) (most relevant current theorem is maxclpr 12011).
Theorem	trilpolemclim 17325*	Lemma for trilpo 17332. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((1 / (2↑𝑛)) · (𝐹‘𝑛)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝ )
Theorem	trilpolemcl 17326*	Lemma for trilpo 17332. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	trilpolemisumle 17327*	Lemma for trilpo 17332. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → Σ𝑖 ∈ 𝑍 ((1 / (2↑𝑖)) · (𝐹‘𝑖)) ≤ Σ𝑖 ∈ 𝑍 (1 / (2↑𝑖)))
Theorem	trilpolemgt1 17328*	Lemma for trilpo 17332. The 1 < 𝐴 case. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → ¬ 1 < 𝐴)
Theorem	trilpolemeq1 17329*	Lemma for trilpo 17332. The 𝐴 = 1 case. This is proved by noting that if any (𝐹‘𝑥) is zero, then the infinite sum 𝐴 is less than one based on the term which is zero. We are using the fact that the 𝐹 sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → 𝐴 = 1)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1)
Theorem	trilpolemlt1 17330*	Lemma for trilpo 17332. The 𝐴 < 1 case. We can use the distance between 𝐴 and one (that is, 1 − 𝐴) to find a position in the sequence 𝑛 where terms after that point will not add up to as much as 1 − 𝐴. By finomni 7487 we know the terms up to 𝑛 either contain a zero or are all one. But if they are all one that contradicts the way we constructed 𝑛, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0)
Theorem	trilpolemres 17331*	Lemma for trilpo 17332. The result. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ (𝜑 → (𝐴 < 1 ∨ 𝐴 = 1 ∨ 1 < 𝐴))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0 ∨ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1))
Theorem	trilpo 17332*	Real number trichotomy implies the Limited Principle of Omniscience (LPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 17330 (which means the sequence contains a zero), trilpolemeq1 17329 (which means the sequence is all ones), and trilpolemgt1 17328 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 17317) or that the real numbers are a discrete field (see trirec0 17333). LPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qtri3or 10692 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ω ∈ Omni)
Theorem	trirec0 17333*	Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy. This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 17332). (Contributed by Jim Kingdon, 10-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ∨ 𝑥 = 0))
Theorem	trirec0xor 17334*	Version of trirec0 17333 with exclusive-or. The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑥 ∈ ℝ (∃𝑧 ∈ ℝ (𝑥 · 𝑧) = 1 ⊻ 𝑥 = 0))
Theorem	apdifflemf 17335	Lemma for apdiff 17337. Being apart from the point halfway between 𝑄 and 𝑅 suffices for 𝐴 to be a different distance from 𝑄 and from 𝑅. (Contributed by Jim Kingdon, 18-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑄 ∈ ℚ)    &   ⊢ (𝜑 → 𝑅 ∈ ℚ)    &   ⊢ (𝜑 → 𝑄 < 𝑅)    &   ⊢ (𝜑 → ((𝑄 + 𝑅) / 2) # 𝐴)    ⇒   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) # (abs‘(𝐴 − 𝑅)))
Theorem	apdifflemr 17336	Lemma for apdiff 17337. (Contributed by Jim Kingdon, 19-May-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑆 ∈ ℚ)    &   ⊢ (𝜑 → (abs‘(𝐴 − -1)) # (abs‘(𝐴 − 1)))    &   ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (abs‘(𝐴 − 0)) # (abs‘(𝐴 − (2 · 𝑆))))    ⇒   ⊢ (𝜑 → 𝐴 # 𝑆)
Theorem	apdiff 17337*	The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.)
⊢ (𝐴 ∈ ℝ → (∀𝑞 ∈ ℚ 𝐴 # 𝑞 ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞 ≠ 𝑟 → (abs‘(𝐴 − 𝑞)) # (abs‘(𝐴 − 𝑟)))))
Theorem	qdiff 17338*	The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 17337 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.)
⊢ (𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
Theorem	iswomninnlem 17339*	Lemma for iswomnimap 7513. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
Theorem	iswomninn 17340*	Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7513 but it will sometimes be more convenient to use 0 and 1 rather than ∅ and 1o. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1))
Theorem	iswomni0 17341*	Weak omniscience stated in terms of equality with 0. Like iswomninn 17340 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ WOmni ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0))
Theorem	ismkvnnlem 17342*	Lemma for ismkvnn 17343. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
Theorem	ismkvnn 17343*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Markov ↔ ∀𝑓 ∈ ({0, 1} ↑𝑚 𝐴)(¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1 → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 0)))
Theorem	redcwlpolemeq1 17344*	Lemma for redcwlpo 17345. A biconditionalized version of trilpolemeq1 17329. (Contributed by Jim Kingdon, 21-Jun-2024.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    ⇒   ⊢ (𝜑 → (𝐴 = 1 ↔ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1))
Theorem	redcwlpo 17345*	Decidability of real number equality implies the Weak Limited Principle of Omniscience (WLPO). We expect that we'd need some form of countable choice to prove the converse. Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 17344). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10696 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 → ω ∈ WOmni)
Theorem	tridceq 17346*	Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 17332 and redcwlpo 17345). Thus, this is an analytic analogue to lpowlpo 7515. (Contributed by Jim Kingdon, 24-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦)
Theorem	redc0 17347*	Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ DECID 𝑥 = 𝑦 ↔ ∀𝑧 ∈ ℝ DECID 𝑧 = 0)
Theorem	reap0 17348*	Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℝ DECID 𝑧 # 0)
Theorem	cndcap 17349*	Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ ℂ DECID 𝑧 # 𝑤)
Theorem	dceqnconst 17350*	Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 17345 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 = 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	dcapnconst 17351*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 17332 for more discussion of decidability of real number apartness. This is a weaker form of dceqnconst 17350 and in fact this theorem can be proved using dceqnconst 17350 as shown at dcapnconstALT 17352. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	dcapnconstALT 17352*	Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 17351 by means of dceqnconst 17350. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ ℝ DECID 𝑥 # 0 → ∃𝑓(𝑓:ℝ⟶ℤ ∧ (𝑓‘0) = 0 ∧ ∀𝑥 ∈ ℝ+ (𝑓‘𝑥) ≠ 0))
Theorem	nconstwlpolem0 17353*	Lemma for nconstwlpo 17356. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ (𝐺‘𝑥) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	nconstwlpolemgt0 17354*	Lemma for nconstwlpo 17356. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℕ (𝐺‘𝑥) = 1)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nconstwlpolem 17355*	Lemma for nconstwlpo 17356. (Contributed by Jim Kingdon, 23-Jul-2024.)
⊢ (𝜑 → 𝐹:ℝ⟶ℤ)    &   ⊢ (𝜑 → (𝐹‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0)    &   ⊢ (𝜑 → 𝐺:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐺‘𝑖))    ⇒   ⊢ (𝜑 → (∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝐺‘𝑦) = 0))
Theorem	nconstwlpo 17356*	Existence of a certain non-constant function from reals to integers implies ω ∈ WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
⊢ (𝜑 → 𝐹:ℝ⟶ℤ)    &   ⊢ (𝜑 → (𝐹‘0) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0)    ⇒   ⊢ (𝜑 → ω ∈ WOmni)
Theorem	neapmkvlem 17357*	Lemma for neapmkv 17358. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
⊢ (𝜑 → 𝐹:ℕ⟶{0, 1})    &   ⊢ 𝐴 = Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝐹‘𝑖))    &   ⊢ ((𝜑 ∧ 𝐴 ≠ 1) → 𝐴 # 1)    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 ∈ ℕ (𝐹‘𝑥) = 1 → ∃𝑥 ∈ ℕ (𝐹‘𝑥) = 0))
Theorem	neapmkv 17358*	If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦) → ω ∈ Markov)
Theorem	neap0mkv 17359*	The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦) ↔ ∀𝑥 ∈ ℝ (𝑥 ≠ 0 → 𝑥 # 0))
Theorem	ltlenmkv 17360*	If < can be expressed as holding exactly when ≤ holds and the values are not equal, then the analytic Markov's Principle applies. (To get the regular Markov's Principle, combine with neapmkv 17358). (Contributed by Jim Kingdon, 23-Feb-2025.)
⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥)) → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≠ 𝑦 → 𝑥 # 𝑦))
14.4.10  Supremum and infimum
Theorem	supfz 17361	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
Theorem	inffz 17362	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
14.4.11  Circle constant
Theorem	taupi 17363	Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)
⊢ τ = (2 · π)
14.5  Mathbox for Mykola Mostovenko
Theorem	ax1hfs 17364	Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)
⊢ (𝜑 → (𝜑 ∧ 𝜑))
14.6  Mathbox for David A. Wheeler
14.6.1  Testable propositions
Theorem	dftest 17365	A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2. We do not formally define testability with a new token, but instead use DECID ¬ before the formula in question. For example, DECID ¬ 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is testable". (Contributed by David A. Wheeler, 13-Aug-2018.) For statements about testable propositions, search for the keyword "testable" in the comments of statements, for instance using the Metamath command "MM> SEARCH * "testable" / COMMENTS". (New usage is discouraged.)
⊢ (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
14.6.2  Allsome quantifier These are definitions and proofs involving the "allsome" quantifier (aka "all some"). In informal language, statements like "All Martians are green" imply that there is at least one Martian. But it's easy to mistranslate informal language into formal notations because similar statements like ∀𝑥𝜑 → 𝜓 do not imply that 𝜑 is ever true, leading to vacuous truths. Some systems include a mechanism to counter this, e.g., PVS allows types to be appended with "+" to declare that they are nonempty. This section presents a different solution to the same problem. The "allsome" quantifier expressly includes the notion of both "all" and "there exists at least one" (aka some), and is defined to make it easier to more directly express both notions. The hope is that if a quantifier more directly expresses this concept, it will be used instead and reduce the risk of creating formal expressions that look okay but in fact are mistranslations. The term "allsome" was chosen because it's short, easy to say, and clearly hints at the two concepts it combines. I do not expect this to be used much in Metamath, because in Metamath there's a general policy of avoiding the use of new definitions unless there are very strong reasons to do so. Instead, my goal is to rigorously define this quantifier and demonstrate a few basic properties of it. The syntax allows two forms that look like they would be problematic, but they are fine. When applied to a top-level implication we allow ∀∃𝑥(𝜑 → 𝜓), and when restricted (applied to a class) we allow ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓). The first symbol after the setvar variable must always be ∈ if it is the form applied to a class, and since ∈ cannot begin a wff, it is unambiguous. The → looks like it would be a problem because 𝜑 or 𝜓 might include implications, but any implication arrow → within any wff must be surrounded by parentheses, so only the implication arrow of ∀∃ can follow the wff. The implication syntax would work fine without the parentheses, but I added the parentheses because it makes things clearer inside larger complex expressions, and it's also more consistent with the rest of the syntax. Naming: "als" is allsome. The form restricted to a class is prefixed with "r", following the way set.mm names the restricted quantifiers it is built from: ∀ gives df-ral 2533 and ∃ gives df-rex 2534, so df-als 17368 (the general form) gives df-rals 17369 (the restricted form). Earlier versions of this material differed, so old references may not match. They wrote the quantifier as an "inverted A" followed by an exclamation point, and they named the general form df-alsi and the restricted form df-alsc. The symbol is now an "inverted A" followed by a "backwards E", which more readers can correctly guess without being taught it. The restricted definition also changed, and the older one was a mistake; see df-rals 17369 for what was wrong with it. This database is intuitionistic, so some of this material differs from its counterpart in set.mm. In particular, a class 𝐴 being inhabited (∃𝑥𝑥 ∈ 𝐴) is a stronger claim here than its being nonempty (𝐴 ≠ ∅); see n0r 3535. The allsome quantifier asserts that a witness exists, which is the stronger notion, so where set.mm states a result using 𝐴 ≠ ∅ the corresponding result here uses inhabitedness instead. Such results are named with a trailing "m", following the convention of r19.2m 3614 and abn0m 3547. Results of set.mm that rely on recovering a witness from 𝐴 ≠ ∅ are omitted, since that step is not available here. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html 3547 I hope that others will eventually agree that allsome is awesome.
Syntax	wals 17366	Extend wff definition to include "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and there is at least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff ∀∃𝑥(𝜑 → 𝜓)
Syntax	wrals 17367	Extend wff definition to include "all some" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
wff ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓)
Definition	df-als 17368	Define "all some" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true and there is at least one 𝑥 where 𝜑 is true. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃𝑥𝜑))
Definition	df-rals 17369	Define "all some" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and there is at least one 𝑥 in 𝐴 where 𝜑 is true. An older definition of the "all some" quantifier when scoped to a class, named df-alsc and now removed, instead applied a bare formula 𝜑 to the members of a class, asserting only (∀𝑥 ∈ 𝐴𝜑 ∧ ∃𝑥𝑥 ∈ 𝐴), that is, that the formula held throughout 𝐴 and that 𝐴 had at least one member. I've now decided that that was a mistake. Its older existence conjunct ∃𝑥𝑥 ∈ 𝐴 did not require any member of 𝐴 to satisfy the antecedent, so if the formula was itself an implication, that inner implication could still be vacuously true, which is precisely what the allsome quantifier exists to prevent. For example, the older definition meant that "among Martians, all tall ones are green" could be considered true if there are Martians, but no tall Martians. This version of the definition instead ensures that claims of the form "among Martians, all tall ones are green" can only be true if all tall Martians are green and that there is at least one tall Martian. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	dfrals2 17370	The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
Theorem	alsd 17371	Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17373 and als2d 17374 taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃𝑥𝜓)    ⇒   ⊢ (𝜑 → ∀∃𝑥(𝜓 → 𝜒))
Theorem	ralsd 17372	Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17375 and rals2d 17376 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   ⊢ (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))
Theorem	als1d 17373	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀∃𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
Theorem	als2d 17374	Deduction rule: Given "all some" applied to a top-level inference, you can extract the "exists" part. (Contributed by David A. Wheeler, 20-Oct-2018.)
⊢ (𝜑 → ∀∃𝑥(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	rals1d 17375	Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
Theorem	rals2d 17376	Deduction rule: Given "all some" applied to a class, you can extract the "there exists" part. Note that the witness must satisfy the antecedent 𝜓, not merely be a member of 𝐴. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	ralsn0d 17377*	Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	ralsmd 17378*	Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17377, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.)
⊢ (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	alsex 17379	The consequent of an "all some" is witnessed: if 𝜓 holds of every 𝑥 satisfying 𝜑, and some 𝑥 satisfies 𝜑, then some 𝑥 satisfies 𝜓. This is the positive counterpart of als-no-surprise 17387, and it is the property that ordinary "for all" with implication lacks: from ∀𝑥(𝜑 → 𝜓) alone nothing whatever follows about 𝜓, since nothing need satisfy 𝜑. It is the allsome quantifier says what a speaker of "all Martians are green" usually means. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (∀∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)
Theorem	ralsex 17380	The consequent of an "all some" restricted to a class is witnessed: some member of 𝐴 satisfying 𝜑 also satisfies 𝜓. Restricted counterpart of alsex 17379. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∃𝑥 ∈ 𝐴 𝜓)
Theorem	alsbii 17381	Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ ∀∃𝑥(𝜒 → 𝜃))
Theorem	ralsbii 17382	Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃𝑥 ∈ 𝐴(𝜒 → 𝜃))
Theorem	alsbid 17383	Deduction form of alsbii 17381. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (∀∃𝑥(𝜓 → 𝜒) ↔ ∀∃𝑥(𝜃 → 𝜏)))
Theorem	nfals 17384	Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃𝑦(𝜑 → 𝜓)
Theorem	nfrals 17385*	Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥∀∃𝑦 ∈ 𝐴(𝜑 → 𝜓)
Theorem	cbvals 17386*	Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (∀∃𝑥(𝜑 → 𝜓) ↔ ∀∃𝑦(𝜒 → 𝜃))
Theorem	als-no-surprise 17387	Demonstrate that there is never a "surprise" when using the allsome quantifier, that is, it is never possible for the consequent to be both always true and always false. This uses the definition of df-als 17368: the universal parts give ∀𝑥¬ 𝜑, which contradicts the witness that the allsome quantifier supplies. Ordinary "for all" with implication has no such property, since ∀𝑥(𝜑 → 𝜓) and ∀𝑥(𝜑 → ¬ 𝜓) can both hold when nothing satisfies 𝜑. (Contributed by David A. Wheeler, 27-Oct-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ ¬ (∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓))
Theorem	rals-no-surprise 17388	Demonstrate that there is never a "surprise" when using the allsome quantifier restricted to a class, that is, it is never possible for the consequent to be both always true and always false of the members of 𝐴 that satisfy the antecedent. This is the restricted counterpart of als-no-surprise 17387, and follows from it by dfrals2 17370. Note that this holds without any assumption that 𝐴 is inhabited; that is the point of allsome, since the corresponding claim for the ordinary restricted "for all" fails when nothing in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 12-Jul-2026.)
⊢ ¬ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∀∃𝑥 ∈ 𝐴(𝜑 → ¬ 𝜓))
Theorem	ralrals 17389	If the universal part of a restricted "all some" statement holds, then the statement reduces to the existence of a member of 𝐴 satisfying its antecedent. This is the restricted counterpart of ralals 17395. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	rexrals 17390	If a member of 𝐴 satisfying the antecedent exists, then a restricted "all some" statement reduces to its universal part. This is the restricted counterpart of rexals 17396. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)))
Theorem	alsanmo 17391	An "all some" statement conjoined with the claim that at most one 𝑥 satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one 𝑥 satisfies the antecedent. The "all some" quantifier supplies the existence of such an 𝑥 and ∃*𝑥𝜑 supplies the at-most-one part, so together they yield ∃!𝑥𝜑. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ ((∀∃𝑥(𝜑 → 𝜓) ∧ ∃*𝑥𝜑) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))
Theorem	ralsanmo 17392	An "all some" statement restricted to a class, conjoined with the claim that at most one 𝑥 in 𝐴 satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one 𝑥 in 𝐴 satisfies the antecedent. This is the restricted counterpart of alsanmo 17391. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
⊢ ((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
Theorem	alsralrex 17393*	The general "all some" quantifier with class membership as its antecedent holds if and only if 𝜑 holds for every 𝑥 in 𝐴 and some 𝑥 in 𝐴 satisfies 𝜑. (Contributed by Peter Mazsa, 27-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	alsraln0m 17394*	The general "all some" quantifier with class membership as its antecedent holds if and only if 𝜑 holds for every 𝑥 in 𝐴 and 𝐴 is inhabited. This is the intuitionistic form of what set.mm states using 𝐴 ≠ ∅; see the section comment. (Contributed by Peter Mazsa, 28-Nov-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))
Theorem	ralals 17395*	If 𝜑 holds for every 𝑥 in 𝐴, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that some 𝑥 in 𝐴 satisfies 𝜑. See ralrals 17389 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑))
Theorem	rexals 17396*	If some 𝑥 in 𝐴 satisfies 𝜑, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that 𝜑 holds for every 𝑥 in 𝐴. See rexrals 17390 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
⊢ (∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	n0alsm 17397*	If 𝐴 is inhabited, then the general "all some" quantifier with class membership as its antecedent reduces to the assertion that 𝜑 holds for every 𝑥 in 𝐴. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
Theorem	2alsraln0m 17398*	Nested general "all some" quantifiers with class membership as their antecedents: 𝜑 holds for every 𝑥 in 𝐴 and every 𝑦 in 𝐵, and both 𝐴 and 𝐵 are inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ (∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)))
Theorem	2alsraln0idm 17399*	Nested general "all some" quantifiers with class membership as their antecedents, for the same class 𝐴: 𝜑 holds for every 𝑥 and every 𝑦 in 𝐴, and 𝐴 is inhabited. (Contributed by Peter Mazsa, 28-May-2019.) (Revised by David A. Wheeler, 20-Jul-2026.)
⊢ (∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐴 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))
14.6.3  Allsome one quantifier These are definitions and proofs involving the "allsome one" quantifier, which extends the "allsome" quantifier of the previous section in the same way that ∃! (df-eu 2089) extends ∃. Some systems extend "there exists" by appending a character to it. If a system provides such an extension, it should provide it for allsome as well: append the same character, let it modify allsome's existence conjunct, and change nothing else. Appending "!" gives "allsome one", so ∀∃!𝑥(𝜑 → 𝜓) means that 𝜓 is true whenever 𝜑 is true and that exactly one 𝑥 satisfies 𝜑. This is what the English word "the" usually does. "The king is hungry" claims that a king exists, that there is only one, and that he is hungry, and the form ∀∃!𝑥(𝜑 → 𝜓) claims exactly that kind of statement (specifically when 𝜑 means 𝑥 is a king and 𝜓 means 𝑥 is hungry). English says all of that in a single phrase, and the first two have a dedicated word ("the") for the construct. Many other languages have their own dedicated way of saying this. Languages reserve that kind of compression for what their speakers need constantly, which is a good reason for a formal notation to be able to say it just as directly, rather than spelling it out afresh as a conjunction of two quantified formulas every time it comes up. Russell analyzed such definite descriptions with this apparatus in "On Denoting", where his example of a phrase that appears to refer to someone but in fact denotes no one at all is "the present King of France", item (1) of [Russell1905] p. 479, France being a republic that has no king. Write "the king is hungry" as ∀𝑥(𝜑 → 𝜓) instead and only the last of those three claims survives. The existence claim is silently gone, since that formula is vacuously true when there is no king, and the uniqueness claim is silently gone as well, since that formula holds just the same when there are five kings. Russell reached the opposite verdict for the same example, remarking that every proposition of the form "the present King of France ..." is false, [Russell1905] p. 482. The reason to care is the reason that motivates allsome, only more so. Note that this is not merely a way of writing ∃!𝑥(𝜑 ∧ 𝜓). Reading 𝜑 as "is a king" and 𝜓 as "is hungry", ∃!𝑥(𝜑 ∧ 𝜓) says that there is exactly one hungry king, whereas ∀∃!𝑥(𝜑 → 𝜓) says that there is exactly one king and that he is hungry. The first is true in a region with five kings exactly one of whom is hungry; the second is false there. Uniqueness attaches to the antecedent, not to the conjunction. See dfalseu2 17417 for the exact relationship between the two and alseueu 17418 for the one direction that does hold. Naming: "alseu" is allsome ("als", as in df-als 17368) extended with "exactly one" ("eu", as in df-eu 2089). The form restricted to a class is prefixed with "r", following df-rals 17369 and df-reu 2535, giving df-ralseu 17403. This database is intuitionistic, but nothing in this section depends on excluded middle, so every statement here has the same form as its counterpart in set.mm. That is unlike the allsome section above, where results that recover a witness from 𝐴 ≠ ∅ are omitted or restated in terms of inhabitedness. Soundness: df-alseu 17402 and df-ralseu 17403 are eliminable and conservative directly, so neither needs a justification theorem. Definitions are required to be eliminable and conservative; see the section comment for df-bi 117. Each is a biconditional whose left side is a new syntax construct (walseu 17400 or wralseu 17401) applied to distinct metavariables, and whose right side uses only constructs introduced earlier (∀, ∃!, ∧, →, and the restricted quantifiers df-ral 2533 and df-reu 2535), so any occurrence of the new construct can be replaced by the right side, which is eliminability. Conservativity follows, since a proof of a statement not mentioning ∀∃! can have every use of the definition replaced in this way. Every variable occurring on the right side already occurs on the left side, so no dummy variable is introduced, and introducing a dummy variable whose choice must be shown not to matter is the only circumstance here that would call for a justification theorem. For more, see "The Allsome Quantifier" by David A. Wheeler at https://dwheeler.com/essays/allsome.html 2535
Syntax	walseu 17400	Extend wff definition to include "all some one" applied to a top-level implication, which means 𝜓 is true whenever 𝜑 is true, and exactly one 𝑥 satisfies 𝜑. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff ∀∃!𝑥(𝜑 → 𝜓)