Theorem zfac 9165

Description: Axiom of Choice expressed with the fewest number of different variables. The penultimate step shows the logical equivalence to ax-ac 9164. (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 9164	. 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	mpbi 219	1 ⊢ ∃𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695

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-ac 9164

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by:  axacndlem4  9311