Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 8-Nov-2026 at 7:16 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
27-Oct-2026psrbagmaxlem1y 15182 Lemma for psrbagmax 15183. All the bags in 𝑌 are (pointwise) less than 𝑆, and thus elements of 𝑍. (Contributed by Jim Kingdon, 27-Oct-2026.)
(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑃:𝐼⟶ℕ0)    &   (𝜑 → 𝑅:𝐼⟶ℕ0)    &   𝑆 = (𝑖 ∈ 𝐼 ↦ sup({(𝑃‘𝑖), (𝑅‘𝑖)}, ℝ, < ))    &   𝑍 = {𝑞 ∈ (ℕ0 ↑𝑚 𝐼) ∣ 𝑞 ∘𝑟 ≤ 𝑆}    &   (𝜑 → ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝑋 (𝑥‘𝑗) ≤ (𝑃‘𝑗))    &   (𝜑 → ∀𝑗 ∈ 𝐼 ∀𝑦 ∈ 𝑌 (𝑦‘𝑗) ≤ (𝑅‘𝑗))    &   (𝜑 → 𝑌 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑌 ∈ Fin)    ⇒   (𝜑 → 𝑌 ⊆ 𝑍)
 
27-Oct-2026psrbagmaxlem1x 15181 Lemma for psrbagmax 15183. All the bags in 𝑋 are (pointwise) less than 𝑆, and thus elements of 𝑍. (Contributed by Jim Kingdon, 27-Oct-2026.)
(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑃:𝐼⟶ℕ0)    &   (𝜑 → 𝑅:𝐼⟶ℕ0)    &   𝑆 = (𝑖 ∈ 𝐼 ↦ sup({(𝑃‘𝑖), (𝑅‘𝑖)}, ℝ, < ))    &   𝑍 = {𝑞 ∈ (ℕ0 ↑𝑚 𝐼) ∣ 𝑞 ∘𝑟 ≤ 𝑆}    &   (𝜑 → ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝑋 (𝑥‘𝑗) ≤ (𝑃‘𝑗))    &   (𝜑 → ∀𝑗 ∈ 𝐼 ∀𝑦 ∈ 𝑌 (𝑦‘𝑗) ≤ (𝑅‘𝑗))    &   (𝜑 → 𝑌 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑌 ∈ Fin)    ⇒   (𝜑 → 𝑋 ⊆ 𝑍)
 
27-Oct-2026psrbagmaxlemfi 15180 Lemma for psrbagmax 15183. Applying psrbaglefifi 15175 to the sets in this theorem. (Contributed by Jim Kingdon, 27-Oct-2026.)
(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑃:𝐼⟶ℕ0)    &   (𝜑 → 𝑅:𝐼⟶ℕ0)    &   𝑆 = (𝑖 ∈ 𝐼 ↦ sup({(𝑃‘𝑖), (𝑅‘𝑖)}, ℝ, < ))    &   𝑍 = {𝑞 ∈ (ℕ0 ↑𝑚 𝐼) ∣ 𝑞 ∘𝑟 ≤ 𝑆}    ⇒   (𝜑 → 𝑍 ∈ Fin)
 
27-Oct-2026psrbagmaxlem1a 15179 Lemma for psrbagmax 15183. A new bag which is the pointwise maximum of two bags. (Contributed by Jim Kingdon, 27-Oct-2026.)
(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    &   (𝜑 → 𝑃:𝐼⟶ℕ0)    &   (𝜑 → 𝑅:𝐼⟶ℕ0)    &   𝑆 = (𝑖 ∈ 𝐼 ↦ sup({(𝑃‘𝑖), (𝑅‘𝑖)}, ℝ, < ))    ⇒   (𝜑 → 𝑆:𝐼⟶ℕ0)
 
27-Oct-2026psrbagmaxlem1 15178 Lemma for psrbagmax 15183. Existence of a bag which is greater than any element of a finite set of bags. (Contributed by Jim Kingdon, 27-Oct-2026.)
(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    ⇒   (𝜑 → ∃𝑝(𝑝:𝐼⟶ℕ0 ∧ ∀𝑗 ∈ 𝐼 ∀𝑥 ∈ 𝑋 (𝑥‘𝑗) ≤ (𝑝‘𝑗)))
 
24-Oct-2026psrbagmax 15183 Given two finite sets of bags, provide a finite set which contains all of their elements.

The proof constructs the result (𝑍 in the lemmas), proves its properties (via psrbagmaxlemfi 15180, psrbagmaxlem1x 15181, and psrbagmaxlem1y 15182), and then this proof combines those lemmas and assigns the result to the variable 𝑧. (Contributed by Jim Kingdon, 24-Oct-2026.)

(𝜑 → 𝑋 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑋 ∈ Fin)    &   (𝜑 → 𝑌 ⊆ (ℕ0 ↑𝑚 𝐼))    &   (𝜑 → 𝑌 ∈ Fin)    &   (𝜑 → 𝐼 ∈ Fin)    ⇒   (𝜑 → ∃𝑧((𝑧 ⊆ (ℕ0 ↑𝑚 𝐼) ∧ 𝑧 ∈ Fin) ∧ (𝑋 ⊆ 𝑧 ∧ 𝑌 ⊆ 𝑧)))
 
24-Oct-2026fsuppfiss 7300 A finitely supported function has a finite subset of its domain such that values outside that subset map to zero. (Contributed by Jim Kingdon, 24-Oct-2026.)
(𝜑 → 𝐹 finSupp 𝑍)    ⇒   (𝜑 → ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝐹 ∧ (𝐹 “ (dom 𝐹 ∖ 𝑤)) ⊆ {𝑍}))
 
22-Oct-2026psrbagfsuppfi 15165 Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by Jim Kingdon, 22-Oct-2026.)
𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ((𝐹 ∈ 𝐷 ∧ 𝐼 ∈ Fin) → 𝐹 finSupp 0)
 
18-Oct-2026suppinisegdc 6513 Relation between the support (𝐹 supp 𝑍) and the initial segment (◡𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.) (Revised by Jim Kingdon, 18-Oct-2026.)
(𝜑 → 𝐹:𝐴⟶𝐵)    &   (𝜑 → 𝐹 ∈ 𝑉)    &   (𝜑 → 𝑍 ∈ 𝐵)    &   (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → (𝐴 ∖ (𝐹 supp 𝑍)) = (◡𝐹 “ {𝑍}))
 
17-Oct-2026funisfsuppdc 7298 The property of a function to be finitely supported (in relation to a given zero). This shows that df-fsuppfi 7293 and df-supp 6480 give the same results, in the case of decidable equality. (Contributed by AV, 23-May-2019.) (Revised by Jim Kingdon, 17-Oct-2026.)
(𝜑 → 𝐹 ∈ 𝑉)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   (𝜑 → 𝑍 ∈ 𝐵)    &   (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)    &   (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → (𝐹 finSupp 𝑍 ↔ (𝐹 supp 𝑍) ∈ Fin))
 
16-Oct-2026isfsuppfid 7297 Deduction form of isfsuppfi 7296. (Contributed by SN, 29-Jul-2024.) (Revised by Jim Kingdon, 16-Oct-2026.)
(𝜑 → 𝑅 ∈ 𝑉)    &   (𝜑 → 𝑍 ∈ 𝑈)    &   (𝜑 → Fun 𝑅)    &   (𝜑 → 𝑊 ∈ Fin)    &   (𝜑 → 𝑊 ⊆ dom 𝑅)    &   (𝜑 → (𝑅 “ (dom 𝑅 ∖ 𝑊)) ⊆ {𝑍})    ⇒   (𝜑 → 𝑅 finSupp 𝑍)
 
16-Oct-2026df-fsuppfi 7293 Define the property of a function to be finitely supported (in relation to a given zero). This definition will perhaps be most useful when the domain of the function has decidable equality; consider as an alternative (𝑅 supp 𝑍) ∈ Fin (see df-supp 6480) which will behave well when a codomain of the function has decidable equality. If both domain and codomain have decidable equality, the two are equivalent as seen at funisfsuppdc 7298. (Contributed by AV, 23-May-2019.) (Revised by Jim Kingdon, 16-Oct-2026.)
finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ ∃𝑤(𝑤 ∈ Fin ∧ 𝑤 ⊆ dom 𝑟 ∧ (𝑟 “ (dom 𝑟 ∖ 𝑤)) ⊆ {𝑧}))}
 
13-Oct-2026mapm 6975 Set exponentiation is inhabited if the base is inhabited. (Contributed by Jim Kingdon, 13-Oct-2026.)
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝐴) → ∃𝑥 𝑥 ∈ (𝐴 ↑𝑚 𝐵))
 
11-Oct-2026psrbagdceq 15167 Finite bags have decidable equality. (Contributed by Jim Kingdon, 11-Oct-2026.)
𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ((𝐼 ∈ Fin ∧ 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷) → DECID 𝐴 = 𝐵)
 
9-Oct-2026ofovex 6311 Applying a function operation to two functions which are sets yields a set. (Contributed by Jim Kingdon, 9-Oct-2026.)
((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘𝑓 𝑅𝐺) ∈ V)
 
8-Oct-2026idjufi 14268 A finite indexed disjoint union of finite sets is finite. (Contributed by Jim Kingdon, 8-Oct-2026.)
(𝜑 → 𝐴 ∈ Fin)    &   ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ Fin)    ⇒   (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ Fin)
 
8-Oct-2026sn0disj 4127 A collection, each of whose elements is empty or a singleton of the index, is disjoint. (Contributed by Jim Kingdon, 8-Oct-2026.)
((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 = ∅ ∨ 𝐵 = {𝑥}))    ⇒   (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
 
6-Oct-2026gsum2dfi 14272 Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) (Revised by Jim Kingdon, 6-Oct-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → Rel 𝐴)    &   (𝜑 → 𝐷 ∈ Fin)    &   (𝜑 → dom 𝐴 ⊆ 𝐷)    &   (𝜑 → dom 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
 
6-Oct-2026relresfin 7270 Restricting to a subset of a finite relation's domain gives a finite set. (Contributed by Jim Kingdon, 6-Oct-2026.)
(𝜑 → 𝐸 ∈ Fin)    &   (𝜑 → Rel 𝐸)    &   (𝜑 → dom 𝐸 ∈ Fin)    &   (𝜑 → 𝐵 ⊆ dom 𝐸)    &   (𝜑 → 𝐵 ∈ Fin)    ⇒   (𝜑 → (𝐸 ↾ 𝐵) ∈ Fin)
 
4-Oct-2026gsum2dfilem2 14271 Lemma for gsum2dfi 14272. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) (Revised by Jim Kingdon, 4-Oct-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → Rel 𝐴)    &   (𝜑 → 𝐷 ∈ Fin)    &   (𝜑 → dom 𝐴 ⊆ 𝐷)    &   (𝜑 → dom 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ dom 𝐴 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
 
2-Oct-2026idjudju 17269 An indexed disjoint union over two sets equals the disjoint union of those two sets. This connects our notation for an indexed disjoint union, ∪ 𝑥 ∈ 𝐶({𝑥} × 𝐹) which uses df-iun 4014, with our notation for the disjoint union of two sets (df-dju 7384). (Contributed by Jim Kingdon, 2-Oct-2026.)
𝐹 = if(𝑥 = ∅, 𝐴, 𝐵)    ⇒   ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) = (𝐴 ⊔ 𝐵)
 
2-Oct-2026gsum2dfilem1 14270 Lemma 1 for gsum2dfi 14272. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) (Revised by Jim Kingdon, 2-Oct-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐴 “ {𝑗}) ∈ Fin)    ⇒   ((𝜑 ∧ 𝑗 ∈ 𝐷) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
 
2-Oct-2026idjusnfi 14269 The image of a singleton through an indexed disjoint union, where it is of finite sets. (Contributed by Jim Kingdon, 2-Oct-2026.)
(𝜑 → 𝐴 ∈ 𝑉)    &   ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ Fin)    &   𝑈 = ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)    ⇒   ((𝜑 ∧ 𝐾 ∈ 𝐴) → (𝑈 “ {𝐾}) ∈ Fin)
 
24-Sep-2026gsumresfi 14262 Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 24-Sep-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   (𝜑 → ∀𝑥 ∈ (𝐴 ∖ 𝑊)(𝐹‘𝑥) = 0 )    &   (𝜑 → 𝑊 ∈ Fin)    &   (𝜑 → 𝑊 ⊆ 𝐴)    ⇒   (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹))
 
23-Sep-2026sineq0re 16093 A complex number whose sine is zero is real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 10-May-2014.) (Revised by Jim Kingdon, 23-Sep-2026.)
((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
 
18-Sep-2026rirrdisj 17308 The rational and irrational numbers are disjoint. Here irrational means apart from any rational number. (Contributed by Jim Kingdon, 18-Sep-2026.)
(ℚ ∩ {𝑥 ∈ ℝ ∣ ∀𝑞 ∈ ℚ 𝑥 # 𝑞}) = ∅
 
18-Sep-2026efnthr 16193 An equation involving an 𝑁-th power. The expression exp(2πi / 𝑁) is a way to write the primitive 𝑁-th root of unity with the smallest positive argument. We could write it as -1↑𝑐(2 / 𝑁) except that we only support positive real numbers as the base for ↑𝑐. The converse is presumably also provable but we do not have a proof yet. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Jim Kingdon, 18-Sep-2026.)
((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) · ((exp‘((i · (2 · π)) / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵))
 
16-Sep-2026cntzm 14160 If the centralizer of a subset of a magma has an element, the magma is inhabited. (Contributed by Jim Kingdon, 16-Sep-2026.)
𝑍 = (Cntz‘𝑀)    ⇒   (𝑋 ∈ (𝑍‘𝑆) → ∃𝑤 𝑤 ∈ 𝑀)
 
16-Sep-2026ressmex 13477 If a structure restriction is inhabited, the structure is a set and so is the class it is restricted to. (Contributed by Jim Kingdon, 16-Sep-2026.)
𝑅 = (𝑊 ↾s 𝐴)    ⇒   (𝑋 ∈ 𝑅 → (𝑊 ∈ V ∧ 𝐴 ∈ V))
 
15-Sep-2026cntzex 14149 Set existence of the centralizer. (Contributed by Jim Kingdon, 15-Sep-2026.)
𝑍 = (Cntz‘𝑀)    ⇒   (𝑀 ∈ 𝑉 → 𝑍 ∈ V)
 
9-Sep-2026flaplt 10738 The floor function value is less than the next integer. (Contributed by NM, 24-Feb-2005.) (Revised by Jim Kingdon, 9-Sep-2026.)
(((𝐴 ∈ ℚ ∨ (𝐴 ∈ ℝ ∧ ∀𝑞 ∈ ℚ 𝐴 # 𝑞)) ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (⌊‘𝐴) < 𝐵))
 
8-Sep-2026fiidxsupcl 12017 A set of integers indexed by a finite set has an upper bound. (Contributed by Jim Kingdon, 8-Sep-2026.)
(𝜑 → 𝐹:𝐴⟶ℤ)    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ≤ 𝑥)
 
6-Sep-2026ofrfidc 7323 Decidability of a relation applied to two functions. (Contributed by Jim Kingdon, 6-Sep-2026.)
(𝜑 → 𝐹 Fn 𝐴)    &   (𝜑 → 𝐺 Fn 𝐴)    &   (𝜑 → ∀𝑥 ∈ 𝐴 DECID (𝐹‘𝑥)𝑅(𝐺‘𝑥))    &   (𝜑 → 𝐴 ∈ Fin)    ⇒   (𝜑 → DECID 𝐹 ∘𝑟 𝑅𝐺)
 
27-Aug-2026prmdcz 12933 Primality is decidable. (Contributed by Jim Kingdon, 27-Aug-2026.)
(𝑁 ∈ ℤ → DECID 𝑁 ∈ ℙ)
 
27-Aug-2026zmincl 12028 The minumum of two integers is an integer. (Contributed by Jim Kingdon, 27-Aug-2026.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → inf({𝐴, 𝐵}, ℝ, < ) ∈ ℤ)
 
25-Aug-2026nn0sqdcq 13012 A nonnegative integer is a perfect square or not. This is similar to nn0sqdc 11167 but expresses the idea of being a perfect square as having a rational number which, when squared, gives the original number. (Contributed by Jim Kingdon, 25-Aug-2026.)
(𝑁 ∈ ℕ0 → DECID ∃𝑞 ∈ ℚ 𝑁 = (𝑞↑2))
 
25-Aug-2026qabscl 11864 The absolute value of a rational number is a rational number. (Contributed by Jim Kingdon, 25-Aug-2026.)
(𝐴 ∈ ℚ → (abs‘𝐴) ∈ ℚ)
 
25-Aug-2026nn0sqdc 11167 A nonnegative integer is a perfect square or not. (Contributed by Jim Kingdon, 25-Aug-2026.)
(𝑁 ∈ ℕ0 → DECID ∃𝑞 ∈ ℕ0 𝑁 = (𝑞↑2))
 
24-Aug-2026sqrtrirr 13013 The square root of a nonnegative integer is either rational or irrational. (Contributed by Jim Kingdon, 24-Aug-2026.)
(𝐴 ∈ ℕ0 → ((√‘𝐴) ∈ ℚ ∨ ((√‘𝐴) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘𝐴) # 𝑞)))
 
21-Aug-2026prmefexple 16325 Convert a bound on a power of a prime to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 21-Aug-2026.)
((𝐴 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((𝐴↑𝑁) ≤ 𝐵 ↔ 𝑁 ≤ (⌊‘((log‘𝐵) / (log‘𝐴)))))
 
20-Aug-2026zprmlogbap 16235 The logarithm of a natural number to a prime base is either rational or irrational.

The proof decomposes 𝑋 into 𝑚 ∈ ℕ and 𝑎 ∈ ℕ0 such that 𝑋 = ((𝐵↑𝑎) · 𝑚) (using nnmaxpw 12977). If 𝑚 = 1 the logarithm is 𝑎, which is rational. If 1 < 𝑚 then we can apply logbgcd1irrap 16223 to show that the logarithm is irrational. (Contributed by Jim Kingdon and Taylor Barrella, 20-Aug-2026.)

((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℙ) → ((𝐵 logb 𝑋) ∈ ℚ ∨ ((𝐵 logb 𝑋) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (𝐵 logb 𝑋) # 𝑞)))
 
20-Aug-2026zprmlogbaplem3 16234 Lemma for zprmlogbap 16235. Decomposing a natural number into a power of a prime base and a factor not divisible by that prime. (Contributed by Jim Kingdon, 20-Aug-2026.)
𝐽 = {𝑧 ∈ ℕ ∣ ¬ 𝐵 ∥ 𝑧}    &   𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((𝐵↑𝑦) · 𝑥))    ⇒   ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℙ) → ∃𝑚 ∈ ℕ ∃𝑎 ∈ ℕ0 (¬ 𝐵 ∥ 𝑚 ∧ 𝑋 = ((𝐵↑𝑎) · 𝑚)))
 
20-Aug-2026zprmlogbaplem2 16233 Lemma for zprmlogbap 16235. The logarithm is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
(𝜑 → 𝐵 ∈ ℙ)    &   (𝜑 → 𝑀 ∈ ℕ)    &   (𝜑 → ¬ 𝐵 ∥ 𝑀)    &   (𝜑 → 𝐴 ∈ ℕ0)    &   𝑋 = ((𝐵↑𝐴) · 𝑀)    ⇒   (𝜑 → ((𝐵 logb 𝑋) ∈ ℚ ∨ ((𝐵 logb 𝑋) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (𝐵 logb 𝑋) # 𝑞)))
 
20-Aug-2026zprmlogbaplem1 16232 Lemma for zprmlogbap 16235. Rearranging an expression involving logarithms. (Contributed by Jim Kingdon, 20-Aug-2026.)
(𝜑 → 𝐵 ∈ ℙ)    &   (𝜑 → 𝑀 ∈ ℕ)    &   (𝜑 → ¬ 𝐵 ∥ 𝑀)    &   (𝜑 → 𝐴 ∈ ℕ0)    ⇒   (𝜑 → (𝐵 logb ((𝐵↑𝐴) · 𝑀)) = (𝐴 + (𝐵 logb 𝑀)))
 
20-Aug-2026flaplelt 10729 A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 20-Aug-2026.)
((𝐴 ∈ ℚ ∨ (𝐴 ∈ ℝ ∧ ∀𝑞 ∈ ℚ 𝐴 # 𝑞)) → ((⌊‘𝐴) ≤ 𝐴 ∧ 𝐴 < ((⌊‘𝐴) + 1)))
 
20-Aug-2026flapcl 10727 The floor (greatest integer) function yields an integer when applied to a number which is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
((𝐴 ∈ ℚ ∨ (𝐴 ∈ ℝ ∧ ∀𝑞 ∈ ℚ 𝐴 # 𝑞)) → (⌊‘𝐴) ∈ ℤ)
 
20-Aug-2026irraddap 10062 The sum of an irrational number and a rational number is irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
(((𝐴 ∈ ℝ ∧ ∀𝑞 ∈ ℚ 𝐴 # 𝑞) ∧ 𝐵 ∈ ℚ) → ((𝐴 + 𝐵) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (𝐴 + 𝐵) # 𝑞))
 
19-Aug-2026nnmaxpw 12977 The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of a base and largest divisor of the number not divisible by that base, is a bijection from pairs of a nonnegative integer and a number not divisible by that base to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.) (Revised by Jim Kingdon, 19-Aug-2026.)
𝐽 = {𝑧 ∈ ℕ ∣ ¬ 𝐵 ∥ 𝑧}    &   𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((𝐵↑𝑦) · 𝑥))    ⇒   (𝐵 ∈ (ℤ≥‘2) → 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ)
 
19-Aug-2026nnmaxpwlemparts 12976 Lemma for nnmaxpw 12977. Decomposing a number into parts. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
(𝐵 ∈ (ℤ≥‘2) → ((((𝑋 ∈ ℕ ∧ ¬ 𝐵 ∥ 𝑋) ∧ 𝑌 ∈ ℕ0) ∧ 𝐴 = ((𝐵↑𝑌) · 𝑋)) ↔ (𝐴 ∈ ℕ ∧ (𝑋 = (𝐴 / (𝐵↑(℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴))))))
 
19-Aug-2026nnmaxpwlemnfac 12975 Lemma for nnmaxpw 12977. Removing the powers of a base from a natural number produces a number not divisible by that base. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ 𝐵 ∥ (𝐴 / (𝐵↑(℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴)))))
 
19-Aug-2026nnmaxpwlemndvds 12974 Lemma for nnmaxpw 12977. A natural number is not divisible by one more than the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐵↑((℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴)) + 1)) ∥ 𝐴)
 
19-Aug-2026nnmaxpwlemdvds 12973 Lemma for nnmaxpw 12977. A natural number is divisible by the highest power of a base which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 19-Aug-2026.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘2)) → (𝐵↑(℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴)
 
18-Aug-2026nnmaxpwlemxy 12972 Lemma for nnmaxpw 12977. Another way of stating that decomposing a natural number into a power of a base and a number not divisible by that base is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
(𝜑 → 𝑋 ∈ ℕ)    &   (𝜑 → 𝐵 ∈ (ℤ≥‘2))    &   (𝜑 → ¬ 𝐵 ∥ 𝑋)    &   (𝜑 → 𝑌 ∈ ℕ0)    &   (𝜑 → 𝐴 = ((𝐵↑𝑌) · 𝑋))    ⇒   (𝜑 → (𝑋 = (𝐴 / (𝐵↑(℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ0 ((𝐵↑𝑧) ∥ 𝐴 ∧ ¬ (𝐵↑(𝑧 + 1)) ∥ 𝐴))))
 
18-Aug-2026pwbdvdseu 12971 A natural number has a unique highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
((𝑁 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘2)) → ∃!𝑚 ∈ ℕ0 ((𝐵↑𝑚) ∥ 𝑁 ∧ ¬ (𝐵↑(𝑚 + 1)) ∥ 𝑁))
 
18-Aug-2026pwbdvdseulemle 12970 Lemma for pwbdvdseu 12971. Powers of a base which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝐴 ∈ ℕ0)    &   (𝜑 → 𝐵 ∈ ℕ0)    &   (𝜑 → 𝑃 ∈ ℕ)    &   (𝜑 → (𝑃↑𝐴) ∥ 𝑁)    &   (𝜑 → ¬ (𝑃↑(𝐵 + 1)) ∥ 𝑁)    ⇒   (𝜑 → 𝐴 ≤ 𝐵)
 
18-Aug-2026pwbdvds 12969 A natural number has a highest power of a base which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) (Revised by Jim Kingdon, 18-Aug-2026.)
((𝑁 ∈ ℕ ∧ 𝐵 ∈ (ℤ≥‘2)) → ∃𝑚 ∈ ℕ0 ((𝐵↑𝑚) ∥ 𝑁 ∧ ¬ (𝐵↑(𝑚 + 1)) ∥ 𝑁))
 
17-Aug-2026pwbdvdslemn 12968 Lemma for pwbdvds 12969. If a natural number has some power of a base which does not divide it, there is a highest power of the base which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) (Revised by Jim Kingdon, 17-Aug-2026.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝐴 ∈ ℕ)    &   (𝜑 → 𝐵 ∈ ℕ)    &   (𝜑 → ¬ (𝐵↑𝐴) ∥ 𝑁)    ⇒   (𝜑 → ∃𝑚 ∈ ℕ0 ((𝐵↑𝑚) ∥ 𝑁 ∧ ¬ (𝐵↑(𝑚 + 1)) ∥ 𝑁))
 
14-Aug-2026reaplog 16114 Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.)
((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 # 𝐵 ↔ (log‘𝐴) # (log‘𝐵)))
 
13-Aug-2026efap1p 16022 If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12487. (Contributed by Jim Kingdon, 13-Aug-2026.)
((𝐴 ∈ ℝ ∧ (1 + 𝐴) # (exp‘𝐴)) → 𝐴 # 0)
 
6-Aug-2026relndmfv 5731 The value of a relation outside its domain is the empty set. (Contributed by Jim Kingdon, 6-Aug-2026.)
((Rel 𝐹 ∧ ¬ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) = ∅)
 
1-Aug-2026wexmiddifxy 17268 Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7204. (Contributed by Jim Kingdon, 1-Aug-2026.)
(WEXMID ↔ ∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∖ 𝑦) ∈ Fin))
 
1-Aug-2026wexmiddifxylem 17267 Lemma for wexmiddifxylem 17267. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
(({1o} ∖ {{𝑥 ∈ 1o ∣ 𝜑}}) ∈ Fin → DECID ¬ 𝜑)
 
31-Jul-2026rabid1o 17256 Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.)
({𝑥 ∈ 1o ∣ 𝜑} = 1o ↔ 𝜑)
 
30-Jul-2026wexmiddc 17264 Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.)
(WEXMID → DECID ¬ 𝜑)
 
30-Jul-2026df-wexmid 17263 Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.)
(WEXMID ↔ ∀𝑝 ∈ 𝒫 1o(¬ 𝑝 = 1o ∨ ¬ ¬ 𝑝 = 1o))
 
29-Jul-2026wexmiddiffi 17266 Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7204. (Contributed by Jim Kingdon, 29-Jul-2026.)
(WEXMID ↔ ∀𝑥∀𝑦(𝑥 ∈ Fin → (𝑥 ∖ 𝑦) ∈ Fin))
 
29-Jul-2026wexmiddiffilem 17265 Lemma for wexmiddiffi 17266. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
(∀𝑥∀𝑦(𝑥 ∈ Fin → (𝑥 ∖ 𝑦) ∈ Fin) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
 
28-Jul-2026psrbaglefifi 15175 There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) (Revised by Jim Kingdon, 28-Jul-2026.)
𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}    ⇒   ((𝐹 ∈ 𝐷 ∧ 𝐼 ∈ Fin) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ Fin)
 
24-Jul-2026stnot 17261 A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.)
(𝐴 ∈ 𝒫 1o → ((¬ ¬ 𝐴 = 1o → 𝐴 = 1o) ↔ ∃𝑦 ∈ 𝒫 1o(𝐴 = 1o ↔ ¬ 𝑦 = 1o)))
 
24-Jul-2026slotm 13472 A structure with an inhabited slot is inhabited. (Contributed by Jim Kingdon, 24-Jul-2026.)
(𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   (𝐴 ∈ (𝐸‘𝐺) → ∃𝑗 𝑗 ∈ 𝐺)
 
22-Jul-2026alseu-no-surprise 17403 Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17371 by alseuals 17389. See als-no-surprise 17371 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
¬ (∀∃!𝑥(𝜑 → 𝜓) ∧ ∀∃!𝑥(𝜑 → ¬ 𝜓))
 
22-Jul-2026alseueu 17402 "The 𝜑 is 𝜓 " implies that exactly one thing is both 𝜑 and 𝜓. This is the half of dfalseu2 17401 that drops the universal conjunct; it does not reverse, so ∃!𝑥(𝜑 ∧ 𝜓) cannot be used in place of an "all some one" statement. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥(𝜑 → 𝜓) → ∃!𝑥(𝜑 ∧ 𝜓))
 
22-Jul-2026dfalseu2 17401 An "all some one" statement is equivalent to its universal part conjoined with the claim that exactly one 𝑥 satisfies both 𝜑 and 𝜓. In other words, given ∀𝑥(𝜑 → 𝜓), requiring exactly one 𝑥 to satisfy 𝜑, which is what df-alseu 17386 requires, and requiring exactly one 𝑥 to satisfy (𝜑 ∧ 𝜓) come to the same thing. Read 𝜑 as "is a king" and 𝜓 as "is hungry": if every king is hungry, then "there is exactly one king" and "there is exactly one hungry king" say the same thing, so either of them, together with "every king is hungry", gives "the king is hungry".

The universal conjunct is what makes that work, and it cannot be dropped. ∃!𝑥(𝜑 ∧ 𝜓) on its own is strictly weaker than ∀∃!𝑥(𝜑 → 𝜓), since it is satisfied when many things are 𝜑 and just one of those is 𝜓, as in a region with five kings exactly one of whom is hungry; see alseueu 17402 for the one direction that does hold without it. Uniqueness attaches to the antecedent, not to the conjunction. Russell's analysis of a definite description is built the same way: its uniqueness clause constrains the description predicate alone, while the predication is a separate conjunct. See his worked example of "the father of Charles II was executed", [Russell1905] p. 482. (Contributed by David A. Wheeler, 22-Jul-2026.)

(∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥(𝜑 ∧ 𝜓)))
 
22-Jul-2026nfralseu 17400 Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17369. (Contributed by David A. Wheeler, 22-Jul-2026.)
Ⅎ𝑥𝐴    &   Ⅎ𝑥𝜑    &   Ⅎ𝑥𝜓    ⇒   Ⅎ𝑥∀∃!𝑦 ∈ 𝐴(𝜑 → 𝜓)
 
22-Jul-2026nfalseu 17399 Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17368. Unlike the set.mm version of this theorem, no disjoint variable condition is needed, because nfeu 2105 here does not require one. (Contributed by David A. Wheeler, 22-Jul-2026.)
Ⅎ𝑥𝜑    &   Ⅎ𝑥𝜓    ⇒   Ⅎ𝑥∀∃!𝑦(𝜑 → 𝜓)
 
22-Jul-2026ralseubii 17398 Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17366. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥 ∈ 𝐴(𝜒 → 𝜃))
 
22-Jul-2026alseubii 17397 Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17365. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃!𝑥(𝜑 → 𝜓) ↔ ∀∃!𝑥(𝜒 → 𝜃))
 
22-Jul-2026ralseu2d 17396 Deduction rule: Given "all some one" applied to a class, you can extract the "exactly one" part. Note that the witness must satisfy the antecedent 𝜓, not merely be a member of 𝐴. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)
 
22-Jul-2026ralseu1d 17395 Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
 
22-Jul-2026alseu2d 17394 Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   (𝜑 → ∃!𝑥𝜓)
 
22-Jul-2026alseu1d 17393 Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀∃!𝑥(𝜓 → 𝜒))    ⇒   (𝜑 → ∀𝑥(𝜓 → 𝜒))
 
22-Jul-2026ralseud 17392 Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17395 and ralseu2d 17396 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)    ⇒   (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))
 
22-Jul-2026alseud 17391 Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 17393 and alseu2d 17394 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀𝑥(𝜓 → 𝜒))    &   (𝜑 → ∃!𝑥𝜓)    ⇒   (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))
 
22-Jul-2026ralseurals 17390 "All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17389. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓))
 
22-Jul-2026alseuals 17389 "All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 17403 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥(𝜑 → 𝜓) → ∀∃𝑥(𝜑 → 𝜓))
 
22-Jul-2026dfralseu2 17388 The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17354. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
 
22-Jul-2026df-ralseu 17387 Define "all some one" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and exactly one 𝑥 in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
 
22-Jul-2026df-alseu 17386 Define "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.)
(∀∃!𝑥(𝜑 → 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))
 
22-Jul-2026wralseu 17385 Extend wff definition to include "all some one" applied to a class, which means 𝜓 is true whenever 𝜑 is true for 𝑥 in 𝐴, and exactly one 𝑥 in 𝐴 satisfies 𝜑. (Contributed by David A. Wheeler, 22-Jul-2026.)
wff ∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓)
 
22-Jul-2026walseu 17384 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 ∀∃!𝑥(𝜑 → 𝜓)
 
22-Jul-2026mptmex 5948 If a function given by maps-to notation is inhabited, then the class it is defined on is inhabited. (Contributed by Jim Kingdon, 22-Jul-2026.)
(𝐶 ∈ (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑦 𝑦 ∈ 𝐴)
 
20-Jul-20262alsraln0idm 17383 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.)
(∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐴 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))
 
20-Jul-20262alsraln0m 17382 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.)
(∀∃𝑥(𝑥 ∈ 𝐴 → ∀∃𝑦(𝑦 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ (∃𝑥 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)))
 
20-Jul-2026n0alsm 17381 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.)
(∃𝑥 𝑥 ∈ 𝐴 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
 
20-Jul-2026alsraln0m 17378 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.)
(∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 𝑥 ∈ 𝐴))
 
20-Jul-2026alsralrex 17377 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.)
(∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑))
 
20-Jul-2026ralsanmo 17376 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 17375. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
 
20-Jul-2026alsanmo 17375 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.)
((∀∃𝑥(𝜑 → 𝜓) ∧ ∃*𝑥𝜑) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∃!𝑥𝜑))
 
20-Jul-2026rexrals 17374 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 17380. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
(∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)))
 
20-Jul-2026ralrals 17373 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 17379. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
(∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∃𝑥 ∈ 𝐴 𝜑))
  Copyright terms: Public domain W3C HTML validation [external]