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

Theorem axacndlem5 10026
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 10025 . . . 4 𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
2 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑥
4 nfnae 2448 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑤
52, 3, 4nf3an 1902 . . . . 5 𝑥(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
6 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑧
7 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑥
8 nfnae 2448 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑤
96, 7, 8nf3an 1902 . . . . . 6 𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
10 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑧
11 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑥
12 nfnae 2448 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑤
1310, 11, 12nf3an 1902 . . . . . . 7 𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
14 nfcvd 2959 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑣)
15 nfcvf 2984 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑧𝑦𝑧)
16153ad2ant1 1130 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑧)
1714, 16nfeld 2969 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑧)
18 nfcvf 2984 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑤𝑦𝑤)
19183ad2ant3 1132 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑤)
2016, 19nfeld 2969 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑧𝑤)
2117, 20nfand 1898 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑧𝑧𝑤))
225, 21nfald 2339 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑥(𝑣𝑧𝑧𝑤))
23 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑧
24 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑥
25 nfnae 2448 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑤
2623, 24, 25nf3an 1902 . . . . . . . . 9 𝑤(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
27 nfv 1915 . . . . . . . . . 10 𝑣(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
2814, 19nfeld 2969 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑤)
29 nfcvf 2984 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
30293ad2ant2 1131 . . . . . . . . . . . . . . 15 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑥)
3119, 30nfeld 2969 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑤𝑥)
3228, 31nfand 1898 . . . . . . . . . . . . 13 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑤𝑤𝑥))
3321, 32nfand 1898 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3426, 33nfexd 2340 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3514, 19nfeqd 2968 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑤)
3634, 35nfbid 1903 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3727, 36nfald 2339 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3826, 37nfexd 2340 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3922, 38nfimd 1895 . . . . . . 7 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
4013, 39nfald 2339 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
41 nfcvd 2959 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑣)
42 nfcvf2 2985 . . . . . . . . . . 11 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
43423ad2ant1 1130 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑦)
4441, 43nfeqd 2968 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑦)
4513, 44nfan1 2199 . . . . . . . 8 𝑧((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
46 nfcvd 2959 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑣)
47 nfcvf2 2985 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥𝑥𝑦)
48473ad2ant2 1131 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑦)
4946, 48nfeqd 2968 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑦)
505, 49nfan1 2199 . . . . . . . . . 10 𝑥((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
51 simpr 488 . . . . . . . . . . . 12 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → 𝑣 = 𝑦)
5251eleq1d 2877 . . . . . . . . . . 11 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑧𝑦𝑧))
5352anbi1d 632 . . . . . . . . . 10 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑧𝑧𝑤) ↔ (𝑦𝑧𝑧𝑤)))
5450, 53albid 2223 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑥(𝑣𝑧𝑧𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
55 nfcvd 2959 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑣)
56 nfcvf2 2985 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑦 𝑦 = 𝑤𝑤𝑦)
57563ad2ant3 1132 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑦)
5855, 57nfeqd 2968 . . . . . . . . . . . . . . . 16 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑦)
5926, 58nfan1 2199 . . . . . . . . . . . . . . 15 𝑤((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
6051eleq1d 2877 . . . . . . . . . . . . . . . . 17 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑤𝑦𝑤))
6160anbi1d 632 . . . . . . . . . . . . . . . 16 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑤𝑤𝑥) ↔ (𝑦𝑤𝑤𝑥)))
6253, 61anbi12d 633 . . . . . . . . . . . . . . 15 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6359, 62exbid 2224 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6451eqeq1d 2803 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣 = 𝑤𝑦 = 𝑤))
6563, 64bibi12d 349 . . . . . . . . . . . . 13 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6665ex 416 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
679, 36, 66cbvald 2420 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6826, 67exbid 2224 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6968adantr 484 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7054, 69imbi12d 348 . . . . . . . 8 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7145, 70albid 2223 . . . . . . 7 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7271ex 416 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
739, 40, 72cbvald 2420 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
745, 73exbid 2224 . . . 4 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
751, 74mpbii 236 . . 3 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
76753exp 1116 . 2 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
77 axacndlem3 10024 . 2 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
78 axacndlem1 10022 . . 3 (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7978aecoms 2442 . 2 (∀𝑦 𝑦 = 𝑥 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
80 nfae 2447 . . . . 5 𝑧𝑦 𝑦 = 𝑤
81 en2lp 9057 . . . . . . . . 9 ¬ (𝑦𝑧𝑧𝑦)
82 elequ2 2127 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑧𝑦𝑧𝑤))
8382anbi2d 631 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑦) ↔ (𝑦𝑧𝑧𝑤)))
8481, 83mtbii 329 . . . . . . . 8 (𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8584sps 2183 . . . . . . 7 (∀𝑦 𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8685pm2.21d 121 . . . . . 6 (∀𝑦 𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8786spsd 2185 . . . . 5 (∀𝑦 𝑦 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8880, 87alrimi 2212 . . . 4 (∀𝑦 𝑦 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8988axc4i 2333 . . 3 (∀𝑦 𝑦 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
908919.8ad 2180 . 2 (∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
9176, 77, 79, 90pm2.61iii 188 1 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wal 1536  wex 1781  wnfc 2939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-13 2382  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-reg 9044  ax-ac 9874
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-eprel 5433  df-fr 5482
This theorem is referenced by:  axacnd  10027
  Copyright terms: Public domain W3C validator