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

Theorem axacndlem5 9377
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 9376 . . . 4 𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
2 nfnae 2317 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3 nfnae 2317 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑥
4 nfnae 2317 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑤
52, 3, 4nf3an 1828 . . . . 5 𝑥(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
6 nfnae 2317 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑧
7 nfnae 2317 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑥
8 nfnae 2317 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑤
96, 7, 8nf3an 1828 . . . . . 6 𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
10 nfnae 2317 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑧
11 nfnae 2317 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑥
12 nfnae 2317 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑤
1310, 11, 12nf3an 1828 . . . . . . 7 𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
14 nfcvd 2762 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑣)
15 nfcvf 2784 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑧𝑦𝑧)
16153ad2ant1 1080 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑧)
1714, 16nfeld 2769 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑧)
18 nfcvf 2784 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑤𝑦𝑤)
19183ad2ant3 1082 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑤)
2016, 19nfeld 2769 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑧𝑤)
2117, 20nfand 1823 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑧𝑧𝑤))
225, 21nfald 2162 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑥(𝑣𝑧𝑧𝑤))
23 nfnae 2317 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑧
24 nfnae 2317 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑥
25 nfnae 2317 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑤
2623, 24, 25nf3an 1828 . . . . . . . . 9 𝑤(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
27 nfv 1840 . . . . . . . . . 10 𝑣(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
2814, 19nfeld 2769 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑤)
29 nfcvf 2784 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
30293ad2ant2 1081 . . . . . . . . . . . . . . 15 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑥)
3119, 30nfeld 2769 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑤𝑥)
3228, 31nfand 1823 . . . . . . . . . . . . 13 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑤𝑤𝑥))
3321, 32nfand 1823 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3426, 33nfexd 2164 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3514, 19nfeqd 2768 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑤)
3634, 35nfbid 1829 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3727, 36nfald 2162 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3826, 37nfexd 2164 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3922, 38nfimd 1820 . . . . . . 7 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
4013, 39nfald 2162 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
41 nfcvd 2762 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑣)
42 nfcvf2 2785 . . . . . . . . . . 11 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
43423ad2ant1 1080 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑦)
4441, 43nfeqd 2768 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑦)
4513, 44nfan1 2066 . . . . . . . 8 𝑧((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
46 nfcvd 2762 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑣)
47 nfcvf2 2785 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥𝑥𝑦)
48473ad2ant2 1081 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑦)
4946, 48nfeqd 2768 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑦)
505, 49nfan1 2066 . . . . . . . . . 10 𝑥((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
51 simpr 477 . . . . . . . . . . . 12 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → 𝑣 = 𝑦)
5251eleq1d 2683 . . . . . . . . . . 11 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑧𝑦𝑧))
5352anbi1d 740 . . . . . . . . . 10 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑧𝑧𝑤) ↔ (𝑦𝑧𝑧𝑤)))
5450, 53albid 2088 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑥(𝑣𝑧𝑧𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
55 nfcvd 2762 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑣)
56 nfcvf2 2785 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑦 𝑦 = 𝑤𝑤𝑦)
57563ad2ant3 1082 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑦)
5855, 57nfeqd 2768 . . . . . . . . . . . . . . . 16 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑦)
5926, 58nfan1 2066 . . . . . . . . . . . . . . 15 𝑤((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
6051eleq1d 2683 . . . . . . . . . . . . . . . . 17 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑤𝑦𝑤))
6160anbi1d 740 . . . . . . . . . . . . . . . 16 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑤𝑤𝑥) ↔ (𝑦𝑤𝑤𝑥)))
6253, 61anbi12d 746 . . . . . . . . . . . . . . 15 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6359, 62exbid 2089 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6451eqeq1d 2623 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣 = 𝑤𝑦 = 𝑤))
6563, 64bibi12d 335 . . . . . . . . . . . . 13 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6665ex 450 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
679, 36, 66cbvald 2276 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6826, 67exbid 2089 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6968adantr 481 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7054, 69imbi12d 334 . . . . . . . 8 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7145, 70albid 2088 . . . . . . 7 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7271ex 450 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
739, 40, 72cbvald 2276 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
745, 73exbid 2089 . . . 4 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
751, 74mpbii 223 . . 3 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
76753exp 1261 . 2 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
77 axacndlem3 9375 . 2 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
78 axacndlem1 9373 . . 3 (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7978aecoms 2311 . 2 (∀𝑦 𝑦 = 𝑥 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
80 nfae 2315 . . . . 5 𝑧𝑦 𝑦 = 𝑤
81 en2lp 8454 . . . . . . . . 9 ¬ (𝑦𝑧𝑧𝑦)
82 elequ2 2001 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑧𝑦𝑧𝑤))
8382anbi2d 739 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑦) ↔ (𝑦𝑧𝑧𝑤)))
8481, 83mtbii 316 . . . . . . . 8 (𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8584sps 2053 . . . . . . 7 (∀𝑦 𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8685pm2.21d 118 . . . . . 6 (∀𝑦 𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8786spsd 2055 . . . . 5 (∀𝑦 𝑦 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8880, 87alrimi 2080 . . . 4 (∀𝑦 𝑦 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8988axc4i 2127 . . 3 (∀𝑦 𝑦 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
90 19.8a 2049 . . 3 (∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
9189, 90syl 17 . 2 (∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
9276, 77, 79, 91pm2.61iii 179 1 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wal 1478  wex 1701  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867  ax-reg 8441  ax-ac 9225
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-eprel 4985  df-fr 5033
This theorem is referenced by:  axacnd  9378
  Copyright terms: Public domain W3C validator