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