Theorem zfac 9876

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 9875. (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 9875	. 2 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣))
2		equequ2 2029	. . . . . . . . . 10 ⊢ (𝑣 = 𝑤 → (𝑢 = 𝑣 ↔ 𝑢 = 𝑤))
3	2	bibi2d 345	. . . . . . . . 9 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
4		elequ2 2125	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑧 ∈ 𝑡 ↔ 𝑧 ∈ 𝑤))
5	4	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ↔ (𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
6		elequ2 2125	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑤))
7		elequ1 2117	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
8	6, 7	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑤 → ((𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥) ↔ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
9	5, 8	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑤 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
10	9	cbvexvw 2040	. . . . . . . . . 10 ⊢ (∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ ∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
11	10	bibi1i 341	. . . . . . . . 9 ⊢ ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤))
12	3, 11	syl6bb 289	. . . . . . . 8 ⊢ (𝑣 = 𝑤 → ((∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
13	12	albidv 1917	. . . . . . 7 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤)))
14		elequ1 2117	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))
15	14	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
16		elequ1 2117	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑦 → (𝑢 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
17	16	anbi1d 631	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑦 → ((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
18	15, 17	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑢 = 𝑦 → (((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
19	18	exbidv 1918	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
20		equequ1 2028	. . . . . . . . 9 ⊢ (𝑢 = 𝑦 → (𝑢 = 𝑤 ↔ 𝑦 = 𝑤))
21	19, 20	bibi12d 348	. . . . . . . 8 ⊢ (𝑢 = 𝑦 → ((∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
22	21	cbvalvw 2039	. . . . . . 7 ⊢ (∀𝑢(∃𝑤((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑢 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
23	13, 22	syl6bb 289	. . . . . 6 ⊢ (𝑣 = 𝑤 → (∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
24	23	cbvexvw 2040	. . . . 5 ⊢ (∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
25	24	imbi2i 338	. . . 4 ⊢ (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
26	25	2albii 1817	. . 3 ⊢ (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
27	26	exbii 1844	. 2 ⊢ (∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑧 ∧ 𝑧 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑥)) ↔ 𝑢 = 𝑣)) ↔ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
28	1, 27	mpbi 232	1 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ac 9875

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  axacndlem4  10026