Theorem zfac 9871

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 9870. (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 9870	. 2 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣))
2		equequ2 2033	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑤))
3	2	bibi2d 346	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
4		elequ2 2126	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑤))
5	4	anbi2d 631	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ↔ (𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
6		elequ2 2126	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤))
7		elequ1 2118	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
8	6, 7	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
9	5, 8	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑤 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
10	9	cbvexvw 2044	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
11	10	bibi1i 342	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤))
12	3, 11	syl6bb 290	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
13	12	albidv 1921	. . . . . . 7 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
14		elequ1 2118	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
15	14	anbi1d 632	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
16		elequ1 2118	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
17	16	anbi1d 632	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
18	15, 17	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑢 = 𝑦 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
19	18	exbidv 1922	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
20		equequ1 2032	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (𝑢 = 𝑤 ↔ 𝑦 = 𝑤))
21	19, 20	bibi12d 349	. . . . . . . 8 ⊢ (𝑢 = 𝑦 → ((∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
22	21	cbvalvw 2043	. . . . . . 7 ⊢ (∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
23	13, 22	syl6bb 290	. . . . . 6 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
24	23	cbvexvw 2044	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
25	24	imbi2i 339	. . . 4 ⊢ (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
26	25	2albii 1822	. . 3 ⊢ (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
27	26	exbii 1849	. 2 ⊢ (∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
28	1, 27	mpbi 233	1 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ac 9870

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  axacndlem4  10021