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 9229
Description: In order to avoid uses of ax-reg 8441 for derivation of AC equivalents, we provide ax-ac2 9229, 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 9231. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1719 available. The derivation of ax-ac2 9229 from ax-ac 9225 is shown by theorem axac2 9232, and the reverse derivation by axac 9233. Note that we use ax-reg 8441 to derive ax-ac 9225 from ax-ac2 9229, but not to derive ax-ac2 9229 from ax-ac 9225. (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 1988 . . . . . . 7 wff 𝑦𝑥
4 vz . . . . . . . . 9 setvar 𝑧
54, 1wel 1988 . . . . . . . 8 wff 𝑧𝑦
6 vv . . . . . . . . . . 11 setvar 𝑣
76, 2wel 1988 . . . . . . . . . 10 wff 𝑣𝑥
81, 6weq 1871 . . . . . . . . . . 11 wff 𝑦 = 𝑣
98wn 3 . . . . . . . . . 10 wff ¬ 𝑦 = 𝑣
107, 9wa 384 . . . . . . . . 9 wff (𝑣𝑥 ∧ ¬ 𝑦 = 𝑣)
114, 6wel 1988 . . . . . . . . 9 wff 𝑧𝑣
1210, 11wa 384 . . . . . . . 8 wff ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣)
135, 12wi 4 . . . . . . 7 wff (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))
143, 13wa 384 . . . . . 6 wff (𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣)))
153wn 3 . . . . . . 7 wff ¬ 𝑦𝑥
164, 2wel 1988 . . . . . . . 8 wff 𝑧𝑥
176, 4wel 1988 . . . . . . . . . 10 wff 𝑣𝑧
186, 1wel 1988 . . . . . . . . . 10 wff 𝑣𝑦
1917, 18wa 384 . . . . . . . . 9 wff (𝑣𝑧𝑣𝑦)
20 vu . . . . . . . . . . . 12 setvar 𝑢
2120, 4wel 1988 . . . . . . . . . . 11 wff 𝑢𝑧
2220, 1wel 1988 . . . . . . . . . . 11 wff 𝑢𝑦
2321, 22wa 384 . . . . . . . . . 10 wff (𝑢𝑧𝑢𝑦)
2420, 6weq 1871 . . . . . . . . . 10 wff 𝑢 = 𝑣
2523, 24wi 4 . . . . . . . . 9 wff ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)
2619, 25wa 384 . . . . . . . 8 wff ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))
2716, 26wi 4 . . . . . . 7 wff (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))
2815, 27wa 384 . . . . . 6 wff 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣))))
2914, 28wo 383 . . . . 5 wff ((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3029, 20wal 1478 . . . 4 wff 𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3130, 6wex 1701 . . 3 wff 𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3231, 4wal 1478 . 2 wff 𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
3332, 1wex 1701 1 wff 𝑦𝑧𝑣𝑢((𝑦𝑥 ∧ (𝑧𝑦 → ((𝑣𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧𝑣))) ∨ (¬ 𝑦𝑥 ∧ (𝑧𝑥 → ((𝑣𝑧𝑣𝑦) ∧ ((𝑢𝑧𝑢𝑦) → 𝑢 = 𝑣)))))
Colors of variables: wff setvar class
This axiom is referenced by:  axac3  9230
  Copyright terms: Public domain W3C validator