Theorem aceq0 10110

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac 10451. (Contributed by NM, 5-Apr-2004.)

Assertion

Ref	Expression
aceq0	⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))

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

Proof of Theorem aceq0

Step	Hyp	Ref	Expression
1		aceq1 10109	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
2		equequ2 2021	. . . . . . . . . 10 ⊢ (𝑣 = 𝑥 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑥))
3	2	bibi2d 342	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
4		elequ2 2113	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑥))
5	4	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
6		elequ2 2113	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑥))
7		elequ1 2105	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
8	6, 7	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
9	5, 8	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
10	9	cbvexvw 2032	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
11	10	bibi1i 338	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥))
12	3, 11	bitrdi 287	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
13	12	albidv 1915	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
14		elequ1 2105	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
15	14	anbi1d 629	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
16		elequ1 2105	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
17	16	anbi1d 629	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
18	15, 17	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑢 = 𝑧 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
19	18	exbidv 1916	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
20		equequ1 2020	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑥 ↔ 𝑧 = 𝑥))
21	19, 20	bibi12d 345	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → ((∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
22	21	cbvalvw 2031	. . . . . . 7 ⊢ (∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
23	13, 22	bitrdi 287	. . . . . 6 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
24	23	cbvexvw 2032	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
25	24	imbi2i 336	. . . 4 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
26	25	2albii 1814	. . 3 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
27	26	exbii 1842	. 2 ⊢ (∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
28	1, 27	bitr4i 278	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1531  ∃wex 1773  ∀wral 3053  ∃wrex 3062  ∃!wreu 3366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-mo 2526  df-eu 2555  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369

This theorem is referenced by:  dfac0  10125  ac2  10453