Theorem aceq0 8824

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

Assertion

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

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

Proof of Theorem aceq0

Step	Hyp	Ref	Expression
1		aceq1 8823	. 2 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
2		equequ2 1940	. . . . . . . . . 10 ⊢ (𝑣 = 𝑥 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑥))
3	2	bibi2d 331	. . . . . . . . 9 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
4		elequ2 1991	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑥))
5	4	anbi2d 736	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
6		elequ2 1991	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑥))
7		elequ1 1984	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦))
8	6, 7	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
9	5, 8	anbi12d 743	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
10	9	cbvexv 2263	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ ∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
11	10	bibi1i 327	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥))
12	3, 11	syl6bb 275	. . . . . . . 8 ⊢ (𝑣 = 𝑥 → ((∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
13	12	albidv 1836	. . . . . . 7 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥)))
14		elequ1 1984	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
15	14	anbi1d 737	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
16		elequ1 1984	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
17	16	anbi1d 737	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → ((𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)))
18	15, 17	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑢 = 𝑧 → (((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
19	18	exbidv 1837	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ ∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦))))
20		equequ1 1939	. . . . . . . . 9 ⊢ (𝑢 = 𝑧 → (𝑢 = 𝑥 ↔ 𝑧 = 𝑥))
21	19, 20	bibi12d 334	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → ((∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ (∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
22	21	cbvalv 2261	. . . . . . 7 ⊢ (∀𝑢(∃𝑥((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑢 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑢 = 𝑥) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
23	13, 22	syl6bb 275	. . . . . 6 ⊢ (𝑣 = 𝑥 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
24	23	cbvexv 2263	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣) ↔ ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥))
25	24	imbi2i 325	. . . 4 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
26	25	2albii 1738	. . 3 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
27	26	exbii 1764	. 2 ⊢ (∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑥∀𝑧(∃𝑥((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ∧ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦)) ↔ 𝑧 = 𝑥)))
28	1, 27	bitr4i 266	1 ⊢ (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-reu 2903

This theorem is referenced by:  dfac0  8838  ac2  9166