Theorem axacndlem4 10629

Description: Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)

Assertion

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

Distinct variable group:   𝑦,𝑧,𝑤

Proof of Theorem axacndlem4

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfac 10479	. . . 4 ⊢ ∃𝑣∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))
2		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
3		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
4		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑤
5	2, 3, 4	nf3an 1901	. . . . 5 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
6		nfnae 2439	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
7		nfnae 2439	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
8		nfnae 2439	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑤
9	6, 7, 8	nf3an 1901	. . . . . 6 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
10		nfnae 2439	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
11		nfnae 2439	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
12		nfnae 2439	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑤
13	10, 11, 12	nf3an 1901	. . . . . . 7 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
14		nfcvf 2926	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦)
15	14	3ad2ant2 1134	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑦)
16		nfcvf 2926	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧)
17	16	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑧)
18	15, 17	nfeld 2911	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 ∈ 𝑧)
19		nfcvf 2926	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤)
20	19	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑤)
21	17, 20	nfeld 2911	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑧 ∈ 𝑤)
22	18, 21	nfand 1897	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))
23		nfnae 2439	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑧
24		nfnae 2439	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦
25		nfnae 2439	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑤
26	23, 24, 25	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑤(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
27	15, 20	nfeld 2911	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 ∈ 𝑤)
28		nfcvd 2900	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑣)
29	20, 28	nfeld 2911	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑤 ∈ 𝑣)
30	27, 29	nfand 1897	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣))
31	22, 30	nfand 1897	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)))
32	26, 31	nfexd 2330	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)))
33	15, 20	nfeqd 2910	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 = 𝑤)
34	32, 33	nfbid 1902	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))
35	9, 34	nfald 2329	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))
36	26, 35	nfexd 2330	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))
37	22, 36	nfimd 1894	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)))
38	13, 37	nfald 2329	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)))
39	9, 38	nfald 2329	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)))
40		nfcvd 2900	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦𝑣)
41		nfcvf2 2927	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
42	41	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦𝑥)
43	40, 42	nfeqd 2910	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑥)
44	9, 43	nfan1 2201	. . . . . . 7 ⊢ Ⅎ𝑦((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
45		nfcvd 2900	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧𝑣)
46		nfcvf2 2927	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥)
47	46	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧𝑥)
48	45, 47	nfeqd 2910	. . . . . . . . 9 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑥)
49	13, 48	nfan1 2201	. . . . . . . 8 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
50	22	nf5rd 2197	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
51	50	adantr 480	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
52		sp 2184	. . . . . . . . . 10 ⊢ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))
53	51, 52	impbid1 225	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
54		nfcvd 2900	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤𝑣)
55		nfcvf2 2927	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → Ⅎ𝑤𝑥)
56	55	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤𝑥)
57	54, 56	nfeqd 2910	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑥)
58	26, 57	nfan1 2201	. . . . . . . . . 10 ⊢ Ⅎ𝑤((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
59		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → 𝑣 = 𝑥)
60	59	eleq2d 2821	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ 𝑥))
61	60	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
62	61	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
63	58, 62	exbid 2224	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
64	63	bibi1d 343	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
65	44, 64	albid 2223	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
66	58, 65	exbid 2224	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
67	53, 66	imbi12d 344	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
68	49, 67	albid 2223	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
69	44, 68	albid 2223	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
70	69	ex 412	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑥 → (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
71	5, 39, 70	cbvexd 2413	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
72	1, 71	mpbii 233	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
73	72	3exp 1119	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
74		axacndlem2 10627	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
75		axacndlem1 10626	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
76		nfae 2438	. . . 4 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑤
77		nfae 2438	. . . . 5 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑤
78		simpr 484	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → 𝑧 ∈ 𝑤)
79	78	alimi 1811	. . . . . 6 ⊢ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥 𝑧 ∈ 𝑤)
80		nd2 10607	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ¬ ∀𝑥 𝑧 ∈ 𝑤)
81	80	pm2.21d 121	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥 𝑧 ∈ 𝑤 → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
82	79, 81	syl5 34	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
83	77, 82	alrimi 2214	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑤 → ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
84	76, 83	alrimi 2214	. . 3 ⊢ (∀𝑥 𝑥 = 𝑤 → ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
85	84	19.8ad 2183	. 2 ⊢ (∀𝑥 𝑥 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
86	73, 74, 75, 85	pm2.61iii 185	1 ⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538  ∃wex 1779  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2377  ax-ext 2708  ax-sep 5271  ax-pr 5407  ax-reg 9611  ax-ac 10478

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  axacndlem5  10630