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 20-Aug-2026 at 7:07 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
14-Aug-2026reaplog 15972 Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.)
((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 # 𝐵 ↔ (log‘𝐴) # (log‘𝐵)))
 
13-Aug-2026efap1p 15882 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 12465. (Contributed by Jim Kingdon, 13-Aug-2026.)
((𝐴 ∈ ℝ ∧ (1 + 𝐴) # (exp‘𝐴)) → 𝐴 # 0)
 
6-Aug-2026relndmfv 5728 The value of a relation outside its domain is the empty set. (Contributed by Jim Kingdon, 6-Aug-2026.)
((Rel 𝐹 ∧ ¬ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) = ∅)
 
1-Aug-2026wexmiddifxy 17058 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 7198. (Contributed by Jim Kingdon, 1-Aug-2026.)
(WEXMID ↔ ∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∖ 𝑦) ∈ Fin))
 
1-Aug-2026wexmiddifxylem 17057 Lemma for wexmiddifxylem 17057. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.)
(({1o} ∖ {{𝑥 ∈ 1o ∣ 𝜑}}) ∈ Fin → DECID ¬ 𝜑)
 
31-Jul-2026rabid1o 17046 Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.)
({𝑥 ∈ 1o ∣ 𝜑} = 1o ↔ 𝜑)
 
30-Jul-2026wexmiddc 17054 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 17053 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 17056 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 7198. (Contributed by Jim Kingdon, 29-Jul-2026.)
(WEXMID ↔ ∀𝑥∀𝑦(𝑥 ∈ Fin → (𝑥 ∖ 𝑦) ∈ Fin))
 
29-Jul-2026wexmiddiffilem 17055 Lemma for wexmiddiffi 17056. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.)
(∀𝑥∀𝑦(𝑥 ∈ Fin → (𝑥 ∖ 𝑦) ∈ Fin) → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
 
24-Jul-2026stnot 17051 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 13417 A structure with an inhabited slot is inhabited. (Contributed by Jim Kingdon, 24-Jul-2026.)
(𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ)    ⇒   (𝐴 ∈ (𝐸‘𝐺) → ∃𝑗 𝑗 ∈ 𝐺)
 
22-Jul-2026alseu-no-surprise 17191 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 17159 by alseuals 17177. See als-no-surprise 17159 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.)
¬ (∀∃!𝑥(𝜑 → 𝜓) ∧ ∀∃!𝑥(𝜑 → ¬ 𝜓))
 
22-Jul-2026alseueu 17190 "The 𝜑 is 𝜓 " implies that exactly one thing is both 𝜑 and 𝜓. This is the half of dfalseu2 17189 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 17189 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 17174 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 17190 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 17188 Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17157. (Contributed by David A. Wheeler, 22-Jul-2026.)
Ⅎ𝑥𝐴    &   Ⅎ𝑥𝜑    &   Ⅎ𝑥𝜓    ⇒   Ⅎ𝑥∀∃!𝑦 ∈ 𝐴(𝜑 → 𝜓)
 
22-Jul-2026nfalseu 17187 Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17156. 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 17186 Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17154. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥 ∈ 𝐴(𝜒 → 𝜃))
 
22-Jul-2026alseubii 17185 Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17153. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃!𝑥(𝜑 → 𝜓) ↔ ∀∃!𝑥(𝜒 → 𝜃))
 
22-Jul-2026ralseu2d 17184 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 17183 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 17182 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 17181 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 17180 Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17183 and ralseu2d 17184 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   (𝜑 → ∃!𝑥 ∈ 𝐴 𝜓)    ⇒   (𝜑 → ∀∃!𝑥 ∈ 𝐴(𝜓 → 𝜒))
 
22-Jul-2026alseud 17179 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 17181 and alseu2d 17182 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.)
(𝜑 → ∀𝑥(𝜓 → 𝜒))    &   (𝜑 → ∃!𝑥𝜓)    ⇒   (𝜑 → ∀∃!𝑥(𝜓 → 𝜒))
 
22-Jul-2026ralseurals 17178 "All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17177. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓))
 
22-Jul-2026alseuals 17177 "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 17191 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥(𝜑 → 𝜓) → ∀∃𝑥(𝜑 → 𝜓))
 
22-Jul-2026dfralseu2 17176 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 17142. (Contributed by David A. Wheeler, 22-Jul-2026.)
(∀∃!𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃!𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
 
22-Jul-2026df-ralseu 17175 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 17174 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 17173 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 17172 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 5945 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 17171 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 17170 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 17169 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 17166 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 17165 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 17164 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 17163. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
((∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃!𝑥 ∈ 𝐴 𝜑))
 
20-Jul-2026alsanmo 17163 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 17162 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 17168. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
(∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)))
 
20-Jul-2026ralrals 17161 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 17167. (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026.)
(∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∃𝑥 ∈ 𝐴 𝜑))
 
20-Jul-2026als-no-surprise 17159 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 17140: 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.)
¬ (∀∃𝑥(𝜑 → 𝜓) ∧ ∀∃𝑥(𝜑 → ¬ 𝜓))
 
20-Jul-2026ralsmd 17150 Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17149, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.)
(𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)
 
19-Jul-2026disjdifg 3598 A class and its relative complement are disjoint. (Contributed by NM, 24-Mar-1998.) Generalize from disjdif 3599. (Revised by BJ, 19-Jul-2026.)
(𝐴 ⊆ 𝐵 → (𝐴 ∩ (𝐶 ∖ 𝐵)) = ∅)
 
19-Jul-2026sseq0b 3564 The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Strengthen sseq0 3565 to a biconditional. (Revised by BJ, 19-Jul-2026.)
(𝐴 = ∅ → (𝐵 ⊆ 𝐴 ↔ 𝐵 = ∅))
 
18-Jul-2026sepab 4278 Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 4279. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.)
(𝐴 ∈ 𝑉 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∈ V)
 
18-Jul-2026inssdif0im 3592 Intersection, subclass, and difference relationship. The converse holds in classical logic but not in intuitionistic logic. (Contributed by Jim Kingdon, 3-Aug-2018.) (Proof shortened by BJ, 18-Jul-2026.)
((𝐴 ∩ 𝐵) ⊆ 𝐶 → (𝐴 ∩ (𝐵 ∖ 𝐶)) = ∅)
 
15-Jul-2026rexals 17168 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 17162 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
(∃𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥 ∈ 𝐴 𝜑))
 
15-Jul-2026ralals 17167 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 17161 for the restricted counterpart. (Contributed by Peter Mazsa, 19-Dec-2018.) (Revised by David A. Wheeler, 15-Jul-2026.)
(∀𝑥 ∈ 𝐴 𝜑 → (∀∃𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑))
 
14-Jul-2026uniex2 4581 The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) (Proof shortened by BJ, 14-Jul-2026.)
∃𝑦 𝑦 = ∪ 𝑥
 
14-Jul-2026sepgi 4252 Inference associated with sepg 4251. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.)
𝐴 ∈ V    ⇒   ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
 
13-Jul-2026f1setfi 7317 The set of injections between two finite sets is finite. (Contributed by Jim Kingdon, 13-Jul-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ Fin)
 
13-Jul-2026fdcf1 7316 It is decidable whether a function from a finite set into another finite set is one-to-one. (Contributed by Jim Kingdon, 13-Jul-2026.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴⟶𝐵) → DECID 𝐹:𝐴–1-1→𝐵)
 
12-Jul-2026rals-no-surprise 17160 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 17159, and follows from it by dfrals2 17142. 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.)
¬ (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ∧ ∀∃𝑥 ∈ 𝐴(𝜑 → ¬ 𝜓))
 
12-Jul-2026cbvals 17158 Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.)
(𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    ⇒   (∀∃𝑥(𝜑 → 𝜓) ↔ ∀∃𝑦(𝜒 → 𝜃))
 
12-Jul-2026nfrals 17157 Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
Ⅎ𝑥𝐴    &   Ⅎ𝑥𝜑    &   Ⅎ𝑥𝜓    ⇒   Ⅎ𝑥∀∃𝑦 ∈ 𝐴(𝜑 → 𝜓)
 
12-Jul-2026nfals 17156 Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
Ⅎ𝑥𝜑    &   Ⅎ𝑥𝜓    ⇒   Ⅎ𝑥∀∃𝑦(𝜑 → 𝜓)
 
12-Jul-2026alsbid 17155 Deduction form of alsbii 17153. (Contributed by David A. Wheeler, 12-Jul-2026.)
Ⅎ𝑥𝜑    &   (𝜑 → (𝜓 ↔ 𝜃))    &   (𝜑 → (𝜒 ↔ 𝜏))    ⇒   (𝜑 → (∀∃𝑥(𝜓 → 𝜒) ↔ ∀∃𝑥(𝜃 → 𝜏)))
 
12-Jul-2026ralsbii 17154 Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃𝑥 ∈ 𝐴(𝜒 → 𝜃))
 
12-Jul-2026alsbii 17153 Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.)
(𝜑 ↔ 𝜒)    &   (𝜓 ↔ 𝜃)    ⇒   (∀∃𝑥(𝜑 → 𝜓) ↔ ∀∃𝑥(𝜒 → 𝜃))
 
12-Jul-2026ralsex 17152 The consequent of an "all some" restricted to a class is witnessed: some member of 𝐴 satisfying 𝜑 also satisfies 𝜓. Restricted counterpart of alsex 17151. (Contributed by David A. Wheeler, 12-Jul-2026.)
(∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) → ∃𝑥 ∈ 𝐴 𝜓)
 
12-Jul-2026alsex 17151 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 17159, 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.)
(∀∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓)
 
12-Jul-2026ralsn0d 17149 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.)
(𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → 𝐴 ≠ ∅)
 
12-Jul-2026rals2d 17148 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.)
(𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
 
12-Jul-2026rals1d 17147 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.)
(𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))    ⇒   (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
 
12-Jul-2026ralsd 17144 Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17147 and rals2d 17148 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.)
(𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))    &   (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    ⇒   (𝜑 → ∀∃𝑥 ∈ 𝐴(𝜓 → 𝜒))
 
12-Jul-2026alsd 17143 Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17145 and als2d 17146 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.)
(𝜑 → ∀𝑥(𝜓 → 𝜒))    &   (𝜑 → ∃𝑥𝜓)    ⇒   (𝜑 → ∀∃𝑥(𝜓 → 𝜒))
 
12-Jul-2026dfrals2 17142 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.)
(∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ ∀∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓))
 
12-Jul-2026df-rals 17141 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.)

(∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∃𝑥 ∈ 𝐴 𝜑))
 
12-Jul-2026wrals 17139 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 ∀∃𝑥 ∈ 𝐴(𝜑 → 𝜓)
 
12-Jul-2026wals 17138 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 ∀∃𝑥(𝜑 → 𝜓)
 
12-Jul-2026vvin 3569 Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3567. (Contributed by BJ, 12-Jul-2026.)
((𝐴 = V ∧ 𝐵 = V) ↔ (𝐴 ∩ 𝐵) = V)
 
7-Jul-2026cmnsubm 14114 A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.)
(𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   (𝜑 → 𝐺 ∈ CMnd)    &   𝐻 = (𝐺 ↾s 𝑆)    ⇒   (𝜑 → 𝐻 ∈ CMnd)
 
29-Jun-2026dichmul0or 16772 Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ ℂ ((𝑧 · 𝑤) = 0 → (𝑧 = 0 ∨ 𝑤 = 0)))
 
29-Jun-2026dichmul0orlem5 16769 Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ((abs‘𝐴) + 𝐴) = 0)    ⇒   (𝜑 → 𝐴 ≤ 0)
 
29-Jun-2026dichmul0orlem4 16768 Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    ⇒   (𝜑 → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) − 𝐴)) = 0)
 
29-Jun-2026dichmul0orlem3 16767 Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))    &   (𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    ⇒   (𝜑 → (𝐴 = 0 ∨ 𝐵 = 0))
 
29-Jun-2026dichmul0orlem2 16766 Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    &   (𝜑 → (abs‘𝐴) ≤ (abs‘𝐵))    ⇒   (𝜑 → 𝐴 = 0)
 
29-Jun-2026dichmul0orlem1 16765 Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑 → 𝐴 ≤ 𝐵)    ⇒   (𝜑 → 𝐴 = 0)
 
29-Jun-2026lealltlt2 16764 Alternative definition for ≤ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → 𝐴 < 𝑥)))
 
29-Jun-2026lealltlt1 16763 Alternative definition for ≤ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ (𝑥 < 𝐴 → 𝑥 < 𝐵)))
 
28-Jun-2026dichmul0orlem7 16771 Lemma for dichmul0or 16772. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0)))    &   (𝜑 → 𝐴 ∈ ℝ)    ⇒   (𝜑 → (𝐴 ≤ 0 ∨ 0 ≤ 𝐴))
 
28-Jun-2026dichmul0orlem6 16770 Lemma for dichmul0or 16772. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ((abs‘𝐴) − 𝐴) = 0)    ⇒   (𝜑 → 0 ≤ 𝐴)
 
28-Jun-2026msq0 8998 A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)
(𝐴 ∈ ℂ → ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0))
 
28-Jun-2026msqap0 8997 A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
(𝐴 ∈ ℂ → ((𝐴 · 𝐴) # 0 ↔ 𝐴 # 0))
 
28-Jun-2026letrid 8442 Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐴 ≤ 𝐵)    &   (𝜑 → 𝐵 ≤ 𝐴)    ⇒   (𝜑 → 𝐴 = 𝐵)
 
19-Jun-2026ringen1zr0 14624 The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14263, and semirings, see srgen1zr0 14294. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    &   𝑍 = (0g‘𝑅)    ⇒   ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
19-Jun-2026srg1zr 14293 The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rngen1zr0 14263 The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    &    0 = (0g‘𝑅)    ⇒   ((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨ 0 , 0 ⟩, 0 ⟩} ∧ ∗ = {⟨⟨ 0 , 0 ⟩, 0 ⟩})))
 
18-Jun-2026rngen1zr 14262 The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rng1zr 14261 The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rng1zrlem 14260 Lemma for rng1zr 14261 and srg1zr 14293. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Mgm ∧ (mulGrp‘𝑅) ∈ Mgm) ∧ ( + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
17-Jun-2026ballotfi 13284 Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    ⇒   (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))
 
17-Jun-2026ballotfilembfi 13241 The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin
 
17-Jun-2026ballotfilemafi 13240 The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin
 
17-Jun-2026ballotfilemefi 13239 𝐸 is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   𝐸 ∈ Fin
 
17-Jun-2026rabxmdc 3554 Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
(∀𝑥 ∈ 𝐴 DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}))
 
15-Jun-2026ballotfilemgun 13270 A property of the defined ↑ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &    ↑ = (𝑢 ∈ 𝑂, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    &   (𝜑 → 𝑈 ∈ 𝑂)    &   (𝜑 → 𝐿 ∈ (𝐽...𝐾))    ⇒   (𝜑 → (𝑈 ↑ (𝐽...𝐾)) = ((𝑈 ↑ (𝐽...(𝐿 − 1))) + (𝑈 ↑ (𝐿...𝐾))))
 
15-Jun-2026ballotfilemgval 13269 Expand the value of ↑. (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &    ↑ = (𝑢 ∈ 𝑂, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    &   (𝜑 → 𝑈 ∈ 𝑂)    &   (𝜑 → 𝐽 ∈ ℤ)    &   (𝜑 → 𝐾 ∈ ℤ)    &   (𝜑 → 𝑉 = (𝐽...𝐾))    ⇒   (𝜑 → (𝑈 ↑ 𝑉) = ((♯‘(𝑉 ∩ 𝑈)) − (♯‘(𝑉 ∖ 𝑈))))
  Copyright terms: Public domain W3C HTML validation [external]