Axiom ax-ac2 10522

Description: In order to avoid uses of ax-reg 9570 for derivation of AC equivalents, we provide ax-ac2 10522, 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 10524. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1828 available. The derivation of ax-ac2 10522 from ax-ac 10518 is shown by Theorem axac2 10525, and the reverse derivation by axac 10526. Note that we use ax-reg 9570 to derive ax-ac 10518 from ax-ac2 10522, but not to derive ax-ac2 10522 from ax-ac 10518. (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 2146	. . . . . . 7 wff 𝑦 ∈ 𝑥
4		vz	. . . . . . . . 9 setvar 𝑧
5	4, 1	wel 2146	. . . . . . . 8 wff 𝑧 ∈ 𝑦
6		vv	. . . . . . . . . . 11 setvar 𝑣
7	6, 2	wel 2146	. . . . . . . . . 10 wff 𝑣 ∈ 𝑥
8	1, 6	weq 1995	. . . . . . . . . . 11 wff 𝑦 = 𝑣
9	8	wn 3	. . . . . . . . . 10 wff ¬ 𝑦 = 𝑣
10	7, 9	wa 401	. . . . . . . . 9 wff (𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣)
11	4, 6	wel 2146	. . . . . . . . 9 wff 𝑧 ∈ 𝑣
12	10, 11	wa 401	. . . . . . . 8 wff ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣)
13	5, 12	wi 4	. . . . . . 7 wff (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))
14	3, 13	wa 401	. . . . . 6 wff (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣)))
15	3	wn 3	. . . . . . 7 wff ¬ 𝑦 ∈ 𝑥
16	4, 2	wel 2146	. . . . . . . 8 wff 𝑧 ∈ 𝑥
17	6, 4	wel 2146	. . . . . . . . . 10 wff 𝑣 ∈ 𝑧
18	6, 1	wel 2146	. . . . . . . . . 10 wff 𝑣 ∈ 𝑦
19	17, 18	wa 401	. . . . . . . . 9 wff (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦)
20		vu	. . . . . . . . . . . 12 setvar 𝑢
21	20, 4	wel 2146	. . . . . . . . . . 11 wff 𝑢 ∈ 𝑧
22	20, 1	wel 2146	. . . . . . . . . . 11 wff 𝑢 ∈ 𝑦
23	21, 22	wa 401	. . . . . . . . . 10 wff (𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦)
24	20, 6	weq 1995	. . . . . . . . . 10 wff 𝑢 = 𝑣
25	23, 24	wi 4	. . . . . . . . 9 wff ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)
26	19, 25	wa 401	. . . . . . . 8 wff ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))
27	16, 26	wi 4	. . . . . . 7 wff (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))
28	15, 27	wa 401	. . . . . 6 wff (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))
29	14, 28	wo 861	. . . . 5 wff ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
30	29, 20	wal 1568	. . . 4 wff ∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
31	30, 6	wex 1812	. . 3 wff ∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
32	31, 4	wal 1568	. 2 wff ∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))
33	32, 1	wex 1812	1 wff ∃𝑦∀𝑧∃𝑣∀𝑢((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣) ∧ 𝑧 ∈ 𝑣))) ∨ (¬ 𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣)))))

This axiom is used by:  axac3  10523