Axiom ax-ac2 9885

Description: In order to avoid uses of ax-reg 9056 for derivation of AC equivalents, we provide ax-ac2 9885, 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 9887. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1796 available. The derivation of ax-ac2 9885 from ax-ac 9881 is shown by theorem axac2 9888, and the reverse derivation by axac 9889. Note that we use ax-reg 9056 to derive ax-ac 9881 from ax-ac2 9885, but not to derive ax-ac2 9885 from ax-ac 9881. (Contributed by NM, 19-Dec-2016.)

Assertion

Ref	Expression
ax-ac2	⊢ ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑣,𝑢

Detailed syntax breakdown of Axiom ax-ac2

Step	Hyp	Ref	Expression
1		vy	. . . . . . . 8 setvar 𝑦
2		vx	. . . . . . . 8 setvar 𝑥
3	1, 2	wel 2115	. . . . . . 7 wff 𝑦 ∈ 𝑥
4		vz	. . . . . . . . 9 setvar 𝑧
5	4, 1	wel 2115	. . . . . . . 8 wff 𝑧 ∈ 𝑦
6		vv	. . . . . . . . . . 11 setvar 𝑣
7	6, 2	wel 2115	. . . . . . . . . 10 wff 𝑣 ∈ 𝑥
8	1, 6	weq 1964	. . . . . . . . . . 11 wff 𝑦 = 𝑣
9	8	wn 3	. . . . . . . . . 10 wff ¬ 𝑦 = 𝑣
10	7, 9	wa 398	. . . . . . . . 9 wff (𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣)
11	4, 6	wel 2115	. . . . . . . . 9 wff 𝑧 ∈ 𝑣
12	10, 11	wa 398	. . . . . . . 8 wff ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣)
13	5, 12	wi 4	. . . . . . 7 wff (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))
14	3, 13	wa 398	. . . . . 6 wff (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣)))
15	3	wn 3	. . . . . . 7 wff ¬ 𝑦 ∈ 𝑥
16	4, 2	wel 2115	. . . . . . . 8 wff 𝑧 ∈ 𝑥
17	6, 4	wel 2115	. . . . . . . . . 10 wff 𝑣 ∈ 𝑧
18	6, 1	wel 2115	. . . . . . . . . 10 wff 𝑣 ∈ 𝑦
19	17, 18	wa 398	. . . . . . . . 9 wff (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)
20		vu	. . . . . . . . . . . 12 setvar 𝑢
21	20, 4	wel 2115	. . . . . . . . . . 11 wff 𝑢 ∈ 𝑧
22	20, 1	wel 2115	. . . . . . . . . . 11 wff 𝑢 ∈ 𝑦
23	21, 22	wa 398	. . . . . . . . . 10 wff (𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦)
24	20, 6	weq 1964	. . . . . . . . . 10 wff 𝑢 = 𝑣
25	23, 24	wi 4	. . . . . . . . 9 wff ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)
26	19, 25	wa 398	. . . . . . . 8 wff ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))
27	16, 26	wi 4	. . . . . . 7 wff (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))
28	15, 27	wa 398	. . . . . 6 wff (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))
29	14, 28	wo 843	. . . . 5 wff ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
30	29, 20	wal 1535	. . . 4 wff ∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
31	30, 6	wex 1780	. . 3 wff ∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
32	31, 4	wal 1535	. 2 wff ∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
33	32, 1	wex 1780	1 wff ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))

This axiom is referenced by:  axac3  9886