Axiom ax-ac2

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vy	⊢ 𝑦
1		vz	⊢ 𝑧
2		vv	⊢ 𝑣
3		vu	⊢ 𝑢
4	0	cv	⊢ 𝑦
5		vx	⊢ 𝑥
6	5	cv	⊢ 𝑥
7	4 6	wcel	⊢ 𝑦 ∈ 𝑥
8	1	cv	⊢ 𝑧
9	8 4	wcel	⊢ 𝑧 ∈ 𝑦
10	2	cv	⊢ 𝑣
11	10 6	wcel	⊢ 𝑣 ∈ 𝑥
12	4 10	wceq	⊢ 𝑦 = 𝑣
13	12	wn	⊢ ¬ 𝑦 = 𝑣
14	11 13	wa	⊢ ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 )
15	8 10	wcel	⊢ 𝑧 ∈ 𝑣
16	14 15	wa	⊢ ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 )
17	9 16	wi	⊢ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) )
18	7 17	wa	⊢ ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
19	7	wn	⊢ ¬ 𝑦 ∈ 𝑥
20	8 6	wcel	⊢ 𝑧 ∈ 𝑥
21	10 8	wcel	⊢ 𝑣 ∈ 𝑧
22	10 4	wcel	⊢ 𝑣 ∈ 𝑦
23	21 22	wa	⊢ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 )
24	3	cv	⊢ 𝑢
25	24 8	wcel	⊢ 𝑢 ∈ 𝑧
26	24 4	wcel	⊢ 𝑢 ∈ 𝑦
27	25 26	wa	⊢ ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 )
28	24 10	wceq	⊢ 𝑢 = 𝑣
29	27 28	wi	⊢ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 )
30	23 29	wa	⊢ ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) )
31	20 30	wi	⊢ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) )
32	19 31	wa	⊢ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
33	18 32	wo	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
34	33 3	wal	⊢ ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
35	34 2	wex	⊢ ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
36	35 1	wal	⊢ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )
37	36 0	wex	⊢ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑦 = 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) )