Theorem aceq0 9805

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 10146. (Contributed by NM, 5-Apr-2004.)

Assertion

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

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

Proof of Theorem aceq0

Step	Hyp	Ref	Expression
1		aceq1 9804	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
2		equequ2 2030	. . . . . . . . . 10 ⊢ (𝑣 = 𝑥 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑥))
3	2	bibi2d 342	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
4		elequ2 2123	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑥))
5	4	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
6		elequ2 2123	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑥))
7		elequ1 2115	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
8	6, 7	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
9	5, 8	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
10	9	cbvexvw 2041	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
11	10	bibi1i 338	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥))
12	3, 11	bitrdi 286	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
13	12	albidv 1924	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
14		elequ1 2115	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
15	14	anbi1d 629	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
16		elequ1 2115	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
17	16	anbi1d 629	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
18	15, 17	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑢 = 𝑧 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
19	18	exbidv 1925	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
20		equequ1 2029	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑥 ↔ 𝑧 = 𝑥))
21	19, 20	bibi12d 345	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → ((∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
22	21	cbvalvw 2040	. . . . . . 7 ⊢ (∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
23	13, 22	bitrdi 286	. . . . . 6 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
24	23	cbvexvw 2041	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
25	24	imbi2i 335	. . . 4 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
26	25	2albii 1824	. . 3 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
27	26	exbii 1851	. 2 ⊢ (∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
28	1, 27	bitr4i 277	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537  ∃wex 1783  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-mo 2540  df-eu 2569  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-reu 3070

This theorem is referenced by:  dfac0  9820  ac2  10148