Metamath Proof Explorer

Theorem ackm

Description: A remarkable equivalent to the Axiom of Choice that has only five quantifiers (when expanded to use only the primitive predicates = and e. and in prenex normal form), discovered and proved by Kurt Maes. This establishes a new record, reducing from 6 to 5 the largest number of quantified variables needed by any ZFC axiom. The ZF-equivalence to AC is shown by Theorem dfackm . Maes found this version of AC in April 2004 (replacing a longer version, also with five quantifiers, that he found in November 2003). See Kurt Maes, "A 5-quantifier ( e. , = )-expression ZF-equivalent to the Axiom of Choice", https://doi.org/10.48550/arXiv.0705.3162 .

The original FOM posts are: http://www.cs.nyu.edu/pipermail/fom/2003-November/007631.html http://www.cs.nyu.edu/pipermail/fom/2003-November/007641.html . (Contributed by NM, 29-Apr-2004) (Revised by Mario Carneiro, 17-May-2015) (Proof modification is discouraged.)

Ref Expression
Assertion ackm ⊢ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v

Proof

Step Hyp Ref Expression
1 axac3 ⊢ CHOICE
2 dfackm ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
3 1 2 mpbi ⊢ ∀ x ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ z ∈ y → v ∈ x ∧ ¬ y = v ∧ z ∈ v ∨ ¬ y ∈ x ∧ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v