MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axacndlem4 Structured version   Visualization version   GIF version

Theorem axacndlem4 9830
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.
StepHypRef Expression
1 zfac 9680 . . . 4 𝑣𝑦𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤))
2 nfnae 2370 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑧
3 nfnae 2370 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑦
4 nfnae 2370 . . . . . 6 𝑥 ¬ ∀𝑥 𝑥 = 𝑤
52, 3, 4nf3an 1864 . . . . 5 𝑥(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
6 nfnae 2370 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑧
7 nfnae 2370 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑦
8 nfnae 2370 . . . . . . 7 𝑦 ¬ ∀𝑥 𝑥 = 𝑤
96, 7, 8nf3an 1864 . . . . . 6 𝑦(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
10 nfnae 2370 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑧
11 nfnae 2370 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
12 nfnae 2370 . . . . . . . 8 𝑧 ¬ ∀𝑥 𝑥 = 𝑤
1310, 11, 12nf3an 1864 . . . . . . 7 𝑧(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
14 nfcvf 2958 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
15143ad2ant2 1114 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑥𝑦)
16 nfcvf 2958 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑧𝑥𝑧)
17163ad2ant1 1113 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑥𝑧)
1815, 17nfeld 2941 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦𝑧)
19 nfcvf 2958 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑤𝑥𝑤)
20193ad2ant3 1115 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑥𝑤)
2117, 20nfeld 2941 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑧𝑤)
2218, 21nfand 1860 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦𝑧𝑧𝑤))
23 nfnae 2370 . . . . . . . . . 10 𝑤 ¬ ∀𝑥 𝑥 = 𝑧
24 nfnae 2370 . . . . . . . . . 10 𝑤 ¬ ∀𝑥 𝑥 = 𝑦
25 nfnae 2370 . . . . . . . . . 10 𝑤 ¬ ∀𝑥 𝑥 = 𝑤
2623, 24, 25nf3an 1864 . . . . . . . . 9 𝑤(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤)
2715, 20nfeld 2941 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦𝑤)
28 nfcvd 2933 . . . . . . . . . . . . . . 15 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑥𝑣)
2920, 28nfeld 2941 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑤𝑣)
3027, 29nfand 1860 . . . . . . . . . . . . 13 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦𝑤𝑤𝑣))
3122, 30nfand 1860 . . . . . . . . . . . 12 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)))
3226, 31nfexd 2269 . . . . . . . . . . 11 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)))
3315, 20nfeqd 2940 . . . . . . . . . . 11 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 = 𝑤)
3432, 33nfbid 1865 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤))
359, 34nfald 2268 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤))
3626, 35nfexd 2269 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤))
3722, 36nfimd 1857 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)))
3813, 37nfald 2268 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)))
399, 38nfald 2268 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑦𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)))
40 nfcvd 2933 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑦𝑣)
41 nfcvf2 2959 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
42413ad2ant2 1114 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑦𝑥)
4340, 42nfeqd 2940 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑥)
449, 43nfan1 2129 . . . . . . 7 𝑦((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
45 nfcvd 2933 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑧𝑣)
46 nfcvf2 2959 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑧𝑧𝑥)
47463ad2ant1 1113 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑧𝑥)
4845, 47nfeqd 2940 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑥)
4913, 48nfan1 2129 . . . . . . . 8 𝑧((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
5022nf5rd 2125 . . . . . . . . . . 11 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑦𝑧𝑧𝑤) → ∀𝑥(𝑦𝑧𝑧𝑤)))
5150adantr 473 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦𝑧𝑧𝑤) → ∀𝑥(𝑦𝑧𝑧𝑤)))
52 sp 2111 . . . . . . . . . 10 (∀𝑥(𝑦𝑧𝑧𝑤) → (𝑦𝑧𝑧𝑤))
5351, 52impbid1 217 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦𝑧𝑧𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
54 nfcvd 2933 . . . . . . . . . . . 12 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑤𝑣)
55 nfcvf2 2959 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑤𝑤𝑥)
56553ad2ant3 1115 . . . . . . . . . . . 12 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → 𝑤𝑥)
5754, 56nfeqd 2940 . . . . . . . . . . 11 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑥)
5826, 57nfan1 2129 . . . . . . . . . 10 𝑤((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥)
59 simpr 477 . . . . . . . . . . . . . . . 16 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → 𝑣 = 𝑥)
6059eleq2d 2851 . . . . . . . . . . . . . . 15 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (𝑤𝑣𝑤𝑥))
6160anbi2d 619 . . . . . . . . . . . . . 14 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦𝑤𝑤𝑣) ↔ (𝑦𝑤𝑤𝑥)))
6261anbi2d 619 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6358, 62exbid 2155 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6463bibi1d 336 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6544, 64albid 2154 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6658, 65exbid 2155 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6753, 66imbi12d 337 . . . . . . . 8 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
6849, 67albid 2154 . . . . . . 7 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
6944, 68albid 2154 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7069ex 405 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑥 → (∀𝑦𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
715, 39, 70cbvexd 2342 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣𝑦𝑧((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
721, 71mpbii 225 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
73723exp 1099 . 2 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
74 axacndlem2 9828 . 2 (∀𝑥 𝑥 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
75 axacndlem1 9827 . 2 (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
76 nfae 2369 . . . 4 𝑦𝑥 𝑥 = 𝑤
77 nfae 2369 . . . . 5 𝑧𝑥 𝑥 = 𝑤
78 simpr 477 . . . . . . 7 ((𝑦𝑧𝑧𝑤) → 𝑧𝑤)
7978alimi 1774 . . . . . 6 (∀𝑥(𝑦𝑧𝑧𝑤) → ∀𝑥 𝑧𝑤)
80 nd2 9808 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ¬ ∀𝑥 𝑧𝑤)
8180pm2.21d 119 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥 𝑧𝑤 → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8279, 81syl5 34 . . . . 5 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8377, 82alrimi 2143 . . . 4 (∀𝑥 𝑥 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8476, 83alrimi 2143 . . 3 (∀𝑥 𝑥 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
858419.8ad 2110 . 2 (∀𝑥 𝑥 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8673, 74, 75, 85pm2.61iii 180 1 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068  wal 1505  wex 1742  wnfc 2916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186  ax-reg 8851  ax-ac 9679
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-v 3417  df-dif 3832  df-un 3834  df-nul 4179  df-sn 4442  df-pr 4444
This theorem is referenced by:  axacndlem5  9831
  Copyright terms: Public domain W3C validator