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

Theorem axacndlem5 10021
Description: Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
Assertion
Ref Expression
axacndlem5 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Distinct variable group:   𝑧,𝑤

Proof of Theorem axacndlem5
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 axacndlem4 10020 . . . 4 𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
2 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑥
4 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑤
52, 3, 4nf3an 1893 . . . . 5 𝑥(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
6 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑧
7 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑥
8 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑤
96, 7, 8nf3an 1893 . . . . . 6 𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
10 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑧
11 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑥
12 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑤
1310, 11, 12nf3an 1893 . . . . . . 7 𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
14 nfcvd 2975 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑣)
15 nfcvf 3004 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑧𝑦𝑧)
16153ad2ant1 1125 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑧)
1714, 16nfeld 2986 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑧)
18 nfcvf 3004 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑤𝑦𝑤)
19183ad2ant3 1127 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑤)
2016, 19nfeld 2986 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑧𝑤)
2117, 20nfand 1889 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑧𝑧𝑤))
225, 21nfald 2338 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑥(𝑣𝑧𝑧𝑤))
23 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑧
24 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑥
25 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑤
2623, 24, 25nf3an 1893 . . . . . . . . 9 𝑤(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
27 nfv 1906 . . . . . . . . . 10 𝑣(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
2814, 19nfeld 2986 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑤)
29 nfcvf 3004 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
30293ad2ant2 1126 . . . . . . . . . . . . . . 15 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑥)
3119, 30nfeld 2986 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑤𝑥)
3228, 31nfand 1889 . . . . . . . . . . . . 13 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑤𝑤𝑥))
3321, 32nfand 1889 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3426, 33nfexd 2339 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3514, 19nfeqd 2985 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑤)
3634, 35nfbid 1894 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3727, 36nfald 2338 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3826, 37nfexd 2339 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3922, 38nfimd 1886 . . . . . . 7 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
4013, 39nfald 2338 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
41 nfcvd 2975 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑣)
42 nfcvf2 3005 . . . . . . . . . . 11 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
43423ad2ant1 1125 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑦)
4441, 43nfeqd 2985 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑦)
4513, 44nfan1 2190 . . . . . . . 8 𝑧((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
46 nfcvd 2975 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑣)
47 nfcvf2 3005 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥𝑥𝑦)
48473ad2ant2 1126 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑦)
4946, 48nfeqd 2985 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑦)
505, 49nfan1 2190 . . . . . . . . . 10 𝑥((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
51 simpr 485 . . . . . . . . . . . 12 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → 𝑣 = 𝑦)
5251eleq1d 2894 . . . . . . . . . . 11 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑧𝑦𝑧))
5352anbi1d 629 . . . . . . . . . 10 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑧𝑧𝑤) ↔ (𝑦𝑧𝑧𝑤)))
5450, 53albid 2214 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑥(𝑣𝑧𝑧𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
55 nfcvd 2975 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑣)
56 nfcvf2 3005 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑦 𝑦 = 𝑤𝑤𝑦)
57563ad2ant3 1127 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑦)
5855, 57nfeqd 2985 . . . . . . . . . . . . . . . 16 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑦)
5926, 58nfan1 2190 . . . . . . . . . . . . . . 15 𝑤((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
6051eleq1d 2894 . . . . . . . . . . . . . . . . 17 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑤𝑦𝑤))
6160anbi1d 629 . . . . . . . . . . . . . . . 16 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑤𝑤𝑥) ↔ (𝑦𝑤𝑤𝑥)))
6253, 61anbi12d 630 . . . . . . . . . . . . . . 15 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6359, 62exbid 2215 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6451eqeq1d 2820 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣 = 𝑤𝑦 = 𝑤))
6563, 64bibi12d 347 . . . . . . . . . . . . 13 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6665ex 413 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
679, 36, 66cbvald 2419 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6826, 67exbid 2215 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6968adantr 481 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7054, 69imbi12d 346 . . . . . . . 8 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7145, 70albid 2214 . . . . . . 7 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7271ex 413 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
739, 40, 72cbvald 2419 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
745, 73exbid 2215 . . . 4 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
751, 74mpbii 234 . . 3 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
76753exp 1111 . 2 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
77 axacndlem3 10019 . 2 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
78 axacndlem1 10017 . . 3 (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7978aecoms 2442 . 2 (∀𝑦 𝑦 = 𝑥 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
80 nfae 2447 . . . . 5 𝑧𝑦 𝑦 = 𝑤
81 en2lp 9057 . . . . . . . . 9 ¬ (𝑦𝑧𝑧𝑦)
82 elequ2 2120 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑧𝑦𝑧𝑤))
8382anbi2d 628 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑦) ↔ (𝑦𝑧𝑧𝑤)))
8481, 83mtbii 327 . . . . . . . 8 (𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8584sps 2174 . . . . . . 7 (∀𝑦 𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8685pm2.21d 121 . . . . . 6 (∀𝑦 𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8786spsd 2176 . . . . 5 (∀𝑦 𝑦 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8880, 87alrimi 2203 . . . 4 (∀𝑦 𝑦 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8988axc4i 2332 . . 3 (∀𝑦 𝑦 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
908919.8ad 2171 . 2 (∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
9176, 77, 79, 90pm2.61iii 186 1 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079  wal 1526  wex 1771  wnfc 2958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-reg 9044  ax-ac 9869
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-eprel 5458  df-fr 5507
This theorem is referenced by:  axacnd  10022
  Copyright terms: Public domain W3C validator