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