MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-ac2 Structured version   Visualization version   GIF version

Axiom ax-ac2 10458
Description: In order to avoid uses of ax-reg 9587 for derivation of AC equivalents, we provide ax-ac2 10458, which is equivalent to the standard AC of textbooks. This appears to be the shortest known equivalent to the standard AC when expressed in terms of set theory primitives. It was found by Kurt Maes as Theorem ackm 10460. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1798 available. The derivation of ax-ac2 10458 from ax-ac 10454 is shown by Theorem axac2 10461, and the reverse derivation by axac 10462. Note that we use ax-reg 9587 to derive ax-ac 10454 from ax-ac2 10458, but not to derive ax-ac2 10458 from ax-ac 10454. (Contributed by NM, 19-Dec-2016.)
Assertion
Ref Expression
ax-ac2 𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑣,𝑢

Detailed syntax breakdown of Axiom ax-ac2
StepHypRef Expression
1 vy . . . . . . . 8 setvar 𝑦
2 vx . . . . . . . 8 setvar 𝑥
31, 2wel 2108 . . . . . . 7 wff 𝑦𝑥
4 vz . . . . . . . . 9 setvar 𝑧
54, 1wel 2108 . . . . . . . 8 wff 𝑧𝑦
6 vv . . . . . . . . . . 11 setvar 𝑣
76, 2wel 2108 . . . . . . . . . 10 wff 𝑣𝑥
81, 6weq 1967 . . . . . . . . . . 11 wff 𝑦 = 𝑣
98wn 3 . . . . . . . . . 10 wff ¬ 𝑦 = 𝑣
107, 9wa 397 . . . . . . . . 9 wff (𝑣𝑥 ∧ ¬ 𝑦 = 𝑣)
114, 6wel 2108 . . . . . . . . 9 wff 𝑧𝑣
1210, 11wa 397 . . . . . . . 8 wff ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣)
135, 12wi 4 . . . . . . 7 wff (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))
143, 13wa 397 . . . . . 6 wff (𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣)))
153wn 3 . . . . . . 7 wff ¬ 𝑦𝑥
164, 2wel 2108 . . . . . . . 8 wff 𝑧𝑥
176, 4wel 2108 . . . . . . . . . 10 wff 𝑣𝑧
186, 1wel 2108 . . . . . . . . . 10 wff 𝑣𝑦
1917, 18wa 397 . . . . . . . . 9 wff (𝑣𝑧𝑣𝑦)
20 vu . . . . . . . . . . . 12 setvar 𝑢
2120, 4wel 2108 . . . . . . . . . . 11 wff 𝑢𝑧
2220, 1wel 2108 . . . . . . . . . . 11 wff 𝑢𝑦
2321, 22wa 397 . . . . . . . . . 10 wff (𝑢𝑧𝑢𝑦)
2420, 6weq 1967 . . . . . . . . . 10 wff 𝑢 = 𝑣
2523, 24wi 4 . . . . . . . . 9 wff ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)
2619, 25wa 397 . . . . . . . 8 wff ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
2716, 26wi 4 . . . . . . 7 wff (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
2815, 27wa 397 . . . . . 6 wff 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2914, 28wo 846 . . . . 5 wff ((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3029, 20wal 1540 . . . 4 wff 𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3130, 6wex 1782 . . 3 wff 𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3231, 4wal 1540 . 2 wff 𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3332, 1wex 1782 1 wff 𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
Colors of variables: wff setvar class
This axiom is referenced by:  axac3  10459
  Copyright terms: Public domain W3C validator