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 𝑥𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 axac3 CHOICE
2 dfackm ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) ) )
3 1 2 mpbi 𝑥𝑦𝑧𝑣𝑢 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑣𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧𝑣 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑣𝑧𝑣𝑦 ) ∧ ( ( 𝑢𝑧𝑢𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )