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

Theorem axacndlem5 9625
 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 9624 . . . 4 𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
2 nfnae 2460 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑧
3 nfnae 2460 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑥
4 nfnae 2460 . . . . . 6 𝑥 ¬ ∀𝑦 𝑦 = 𝑤
52, 3, 4nf3an 1980 . . . . 5 𝑥(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
6 nfnae 2460 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑧
7 nfnae 2460 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑥
8 nfnae 2460 . . . . . . 7 𝑦 ¬ ∀𝑦 𝑦 = 𝑤
96, 7, 8nf3an 1980 . . . . . 6 𝑦(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
10 nfnae 2460 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑧
11 nfnae 2460 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑥
12 nfnae 2460 . . . . . . . 8 𝑧 ¬ ∀𝑦 𝑦 = 𝑤
1310, 11, 12nf3an 1980 . . . . . . 7 𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
14 nfcvd 2903 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑣)
15 nfcvf 2926 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑧𝑦𝑧)
16153ad2ant1 1128 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑧)
1714, 16nfeld 2911 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑧)
18 nfcvf 2926 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑤𝑦𝑤)
19183ad2ant3 1130 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑤)
2016, 19nfeld 2911 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑧𝑤)
2117, 20nfand 1975 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑧𝑧𝑤))
225, 21nfald 2310 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑥(𝑣𝑧𝑧𝑤))
23 nfnae 2460 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑧
24 nfnae 2460 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑥
25 nfnae 2460 . . . . . . . . . 10 𝑤 ¬ ∀𝑦 𝑦 = 𝑤
2623, 24, 25nf3an 1980 . . . . . . . . 9 𝑤(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
27 nfv 1992 . . . . . . . . . 10 𝑣(¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤)
2814, 19nfeld 2911 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣𝑤)
29 nfcvf 2926 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥𝑦𝑥)
30293ad2ant2 1129 . . . . . . . . . . . . . . 15 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑦𝑥)
3119, 30nfeld 2911 . . . . . . . . . . . . . 14 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑤𝑥)
3228, 31nfand 1975 . . . . . . . . . . . . 13 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(𝑣𝑤𝑤𝑥))
3321, 32nfand 1975 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3426, 33nfexd 2312 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)))
3514, 19nfeqd 2910 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑤)
3634, 35nfbid 1981 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3727, 36nfald 2310 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3826, 37nfexd 2312 . . . . . . . 8 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤))
3922, 38nfimd 1972 . . . . . . 7 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
4013, 39nfald 2310 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑦𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)))
41 nfcvd 2903 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑣)
42 nfcvf2 2927 . . . . . . . . . . 11 (¬ ∀𝑦 𝑦 = 𝑧𝑧𝑦)
43423ad2ant1 1128 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑧𝑦)
4441, 43nfeqd 2910 . . . . . . . . 9 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑦)
4513, 44nfan1 2215 . . . . . . . 8 𝑧((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
46 nfcvd 2903 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑣)
47 nfcvf2 2927 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥𝑥𝑦)
48473ad2ant2 1129 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑥𝑦)
4946, 48nfeqd 2910 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑦)
505, 49nfan1 2215 . . . . . . . . . 10 𝑥((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
51 simpr 479 . . . . . . . . . . . 12 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → 𝑣 = 𝑦)
5251eleq1d 2824 . . . . . . . . . . 11 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑧𝑦𝑧))
5352anbi1d 743 . . . . . . . . . 10 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑧𝑧𝑤) ↔ (𝑦𝑧𝑧𝑤)))
5450, 53albid 2237 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑥(𝑣𝑧𝑧𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
55 nfcvd 2903 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑣)
56 nfcvf2 2927 . . . . . . . . . . . . . . . . . 18 (¬ ∀𝑦 𝑦 = 𝑤𝑤𝑦)
57563ad2ant3 1130 . . . . . . . . . . . . . . . . 17 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → 𝑤𝑦)
5855, 57nfeqd 2910 . . . . . . . . . . . . . . . 16 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑦)
5926, 58nfan1 2215 . . . . . . . . . . . . . . 15 𝑤((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦)
6051eleq1d 2824 . . . . . . . . . . . . . . . . 17 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣𝑤𝑦𝑤))
6160anbi1d 743 . . . . . . . . . . . . . . . 16 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((𝑣𝑤𝑤𝑥) ↔ (𝑦𝑤𝑤𝑥)))
6253, 61anbi12d 749 . . . . . . . . . . . . . . 15 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6359, 62exbid 2238 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6451eqeq1d 2762 . . . . . . . . . . . . . 14 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (𝑣 = 𝑤𝑦 = 𝑤))
6563, 64bibi12d 334 . . . . . . . . . . . . 13 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6665ex 449 . . . . . . . . . . . 12 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → ((∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
679, 36, 66cbvald 2422 . . . . . . . . . . 11 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6826, 67exbid 2238 . . . . . . . . . 10 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6968adantr 472 . . . . . . . . 9 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7054, 69imbi12d 333 . . . . . . . 8 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → ((∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7145, 70albid 2237 . . . . . . 7 (((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) ∧ 𝑣 = 𝑦) → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
7271ex 449 . . . . . 6 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (𝑣 = 𝑦 → (∀𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
739, 40, 72cbvald 2422 . . . . 5 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∀𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
745, 73exbid 2238 . . . 4 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → (∃𝑥𝑣𝑧(∀𝑥(𝑣𝑧𝑧𝑤) → ∃𝑤𝑣(∃𝑤((𝑣𝑧𝑧𝑤) ∧ (𝑣𝑤𝑤𝑥)) ↔ 𝑣 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
751, 74mpbii 223 . . 3 ((¬ ∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
76753exp 1113 . 2 (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
77 axacndlem3 9623 . 2 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
78 axacndlem1 9621 . . 3 (∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7978aecoms 2454 . 2 (∀𝑦 𝑦 = 𝑥 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
80 nfae 2458 . . . . 5 𝑧𝑦 𝑦 = 𝑤
81 en2lp 8675 . . . . . . . . 9 ¬ (𝑦𝑧𝑧𝑦)
82 elequ2 2153 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑧𝑦𝑧𝑤))
8382anbi2d 742 . . . . . . . . 9 (𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑦) ↔ (𝑦𝑧𝑧𝑤)))
8481, 83mtbii 315 . . . . . . . 8 (𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8584sps 2202 . . . . . . 7 (∀𝑦 𝑦 = 𝑤 → ¬ (𝑦𝑧𝑧𝑤))
8685pm2.21d 118 . . . . . 6 (∀𝑦 𝑦 = 𝑤 → ((𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8786spsd 2204 . . . . 5 (∀𝑦 𝑦 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8880, 87alrimi 2229 . . . 4 (∀𝑦 𝑦 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8988axc4i 2278 . . 3 (∀𝑦 𝑦 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
90 19.8a 2199 . . 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 383   ∧ w3a 1072  ∀wal 1630  ∃wex 1853  Ⅎwnfc 2889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-reg 8662  ax-ac 9473 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-eprel 5179  df-fr 5225 This theorem is referenced by:  axacnd  9626
 Copyright terms: Public domain W3C validator