Theorem zfac 10531

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 10530. (New usage is discouraged.) (Contributed by NM, 14-Aug-2003.)

Assertion

Ref	Expression
zfac	⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Proof of Theorem zfac

Dummy variables 𝑣 𝑢 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ac 10530	. 2 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣))
2		equequ2 2059	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑤))
3	2	bibi2d 345	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
4		elequ2 2160	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑤))
5	4	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ↔ (𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
6		elequ2 2160	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤))
7		elequ1 2152	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
8	6, 7	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
9	5, 8	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑤 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
10	9	cbvexvw 2070	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
11	10	bibi1i 341	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤))
12	3, 11	bitrdi 290	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
13	12	albidv 1953	. . . . . . 7 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
14		elequ1 2152	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
15	14	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
16		elequ1 2152	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
17	16	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
18	15, 17	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑢 = 𝑦 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
19	18	exbidv 1954	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
20		equequ1 2058	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (𝑢 = 𝑤 ↔ 𝑦 = 𝑤))
21	19, 20	bibi12d 348	. . . . . . . 8 ⊢ (𝑢 = 𝑦 → ((∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
22	21	cbvalvw 2069	. . . . . . 7 ⊢ (∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
23	13, 22	bitrdi 290	. . . . . 6 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
24	23	cbvexvw 2070	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
25	24	imbi2i 339	. . . 4 ⊢ (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
26	25	2albii 1853	. . 3 ⊢ (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
27	26	exbii 1881	. 2 ⊢ (∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
28	1, 27	mpbi 233	1 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ac 10530

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  axacndlem4  10688