Step | Hyp | Ref
| Expression |
1 | | axpowndlem3 10100 |
. . . . 5
⊢ (¬
𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
2 | 1 | ax-gen 1802 |
. . . 4
⊢
∀𝑤(¬
𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
3 | | nfnae 2433 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑥 |
4 | | nfnae 2433 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑦 𝑦 = 𝑧 |
5 | 3, 4 | nfan 1905 |
. . . . 5
⊢
Ⅎ𝑦(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
6 | | nfcvf 2928 |
. . . . . . . . 9
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥) |
7 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑥) |
8 | | nfcvd 2900 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑤) |
9 | 7, 8 | nfeqd 2909 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑥 = 𝑤) |
10 | 9 | nfnd 1864 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 ¬ 𝑥 = 𝑤) |
11 | | nfnae 2433 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑥 |
12 | | nfnae 2433 |
. . . . . . . 8
⊢
Ⅎ𝑥 ¬
∀𝑦 𝑦 = 𝑧 |
13 | 11, 12 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑥(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
14 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑤(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
15 | | nfnae 2433 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑥 |
16 | | nfnae 2433 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧 ¬
∀𝑦 𝑦 = 𝑧 |
17 | 15, 16 | nfan 1905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧(¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) |
18 | 7, 8 | nfeld 2910 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑥 ∈ 𝑤) |
19 | 17, 18 | nfexd 2330 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∃𝑧 𝑥 ∈ 𝑤) |
20 | | nfcvf 2928 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑦𝑧) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦𝑧) |
22 | 7, 21 | nfeld 2910 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑥 ∈ 𝑧) |
23 | 14, 22 | nfald 2329 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑤 𝑥 ∈ 𝑧) |
24 | 19, 23 | nfimd 1900 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧)) |
25 | 13, 24 | nfald 2329 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧)) |
26 | 8, 7 | nfeld 2910 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦 𝑤 ∈ 𝑥) |
27 | 25, 26 | nfimd 1900 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
28 | 14, 27 | nfald 2329 |
. . . . . . 7
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
29 | 13, 28 | nfexd 2330 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) |
30 | 10, 29 | nfimd 1900 |
. . . . 5
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦(¬ 𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥))) |
31 | | equequ2 2037 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑥 = 𝑤 ↔ 𝑥 = 𝑦)) |
32 | 31 | notbid 321 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (¬ 𝑥 = 𝑤 ↔ ¬ 𝑥 = 𝑦)) |
33 | 32 | adantl 485 |
. . . . . . 7
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (¬ 𝑥 = 𝑤 ↔ ¬ 𝑥 = 𝑦)) |
34 | | nfcvd 2900 |
. . . . . . . . . . . . . . 15
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥𝑤) |
35 | | nfcvf2 2929 |
. . . . . . . . . . . . . . . 16
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑥𝑦) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥𝑦) |
37 | 34, 36 | nfeqd 2909 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑥 𝑤 = 𝑦) |
38 | 13, 37 | nfan1 2201 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) |
39 | | nfcvd 2900 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧𝑤) |
40 | | nfcvf2 2929 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧𝑦) |
41 | 40 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧𝑦) |
42 | 39, 41 | nfeqd 2909 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑦) |
43 | 17, 42 | nfan1 2201 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) |
44 | | elequ2 2128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
45 | 44 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
46 | 43, 45 | exbid 2224 |
. . . . . . . . . . . . . 14
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∃𝑧 𝑥 ∈ 𝑤 ↔ ∃𝑧 𝑥 ∈ 𝑦)) |
47 | | biidd 265 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))) |
49 | 5, 22, 48 | cbvald 2406 |
. . . . . . . . . . . . . . 15
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑤 𝑥 ∈ 𝑧 ↔ ∀𝑦 𝑥 ∈ 𝑧)) |
50 | 49 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑤 𝑥 ∈ 𝑧 ↔ ∀𝑦 𝑥 ∈ 𝑧)) |
51 | 46, 50 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) ↔ (∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧))) |
52 | 38, 51 | albid 2223 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) ↔ ∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧))) |
53 | | elequ1 2120 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
54 | 53 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
55 | 52, 54 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
56 | 55 | ex 416 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → ((∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
57 | 5, 27, 56 | cbvald 2406 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
58 | 13, 57 | exbid 2224 |
. . . . . . . 8
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
59 | 58 | adantr 484 |
. . . . . . 7
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
60 | 33, 59 | imbi12d 348 |
. . . . . 6
⊢ (((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ((¬ 𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) ↔ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
61 | 60 | ex 416 |
. . . . 5
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → ((¬ 𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) ↔ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))))) |
62 | 5, 30, 61 | cbvald 2406 |
. . . 4
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑤(¬ 𝑥 = 𝑤 → ∃𝑥∀𝑤(∀𝑥(∃𝑧 𝑥 ∈ 𝑤 → ∀𝑤 𝑥 ∈ 𝑧) → 𝑤 ∈ 𝑥)) ↔ ∀𝑦(¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
63 | 2, 62 | mpbii 236 |
. . 3
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑦(¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
64 | 63 | 19.21bi 2189 |
. 2
⊢ ((¬
∀𝑦 𝑦 = 𝑥 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
65 | 64 | ex 416 |
1
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |