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