Step | Hyp | Ref
| Expression |
1 | | zfpow 5233 |
. . . 4
⊢
∃𝑤∀𝑦(∀𝑤(𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) |
2 | | 19.8a 2182 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑦 → ∃𝑧 𝑤 ∈ 𝑦) |
3 | | sp 2184 |
. . . . . . . 8
⊢
(∀𝑦 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧) |
4 | 2, 3 | imim12i 62 |
. . . . . . 7
⊢
((∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧)) |
5 | 4 | alimi 1818 |
. . . . . 6
⊢
(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧)) |
6 | 5 | imim1i 63 |
. . . . 5
⊢
((∀𝑤(𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) → (∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
7 | 6 | alimi 1818 |
. . . 4
⊢
(∀𝑦(∀𝑤(𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) → ∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
8 | 1, 7 | eximii 1843 |
. . 3
⊢
∃𝑤∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) |
9 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
10 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
11 | 9, 10 | nfan 1906 |
. . . 4
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
12 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
13 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
14 | 12, 13 | nfan 1906 |
. . . . 5
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
15 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑤(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
16 | | nfnae 2434 |
. . . . . . . . . 10
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
17 | | nfcvd 2900 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑤) |
18 | | nfcvf 2928 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
19 | 17, 18 | nfeld 2910 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) |
20 | 16, 19 | nfexd 2331 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∃𝑧 𝑤 ∈ 𝑦) |
21 | 20 | adantr 484 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑧 𝑤 ∈ 𝑦) |
22 | | nfcvd 2900 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑤) |
23 | | nfcvf 2928 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
24 | 22, 23 | nfeld 2910 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑤 ∈ 𝑧) |
25 | 13, 24 | nfald 2330 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥∀𝑦 𝑤 ∈ 𝑧) |
26 | 25 | adantl 485 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦 𝑤 ∈ 𝑧) |
27 | 21, 26 | nfimd 1901 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧)) |
28 | 15, 27 | nfald 2330 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧)) |
29 | 18, 17 | nfeld 2910 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑤) |
30 | 29 | adantr 484 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑤) |
31 | 28, 30 | nfimd 1901 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
32 | 14, 31 | nfald 2330 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
33 | | nfeqf2 2377 |
. . . . . . . . 9
⊢ (¬
∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑤 = 𝑥) |
34 | 33 | naecoms 2429 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = 𝑥) |
35 | 34 | adantr 484 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥) |
36 | 14, 35 | nfan1 2202 |
. . . . . 6
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
37 | | nfnae 2434 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑧 |
38 | | nfeqf2 2377 |
. . . . . . . . . . . . . . 15
⊢ (¬
∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧 𝑤 = 𝑥) |
39 | 38 | naecoms 2429 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑥) |
40 | 37, 39 | nfan1 2202 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧(¬
∀𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥) |
41 | | elequ1 2121 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥) → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
43 | 40, 42 | exbid 2225 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ 𝑤 = 𝑥) → (∃𝑧 𝑤 ∈ 𝑦 ↔ ∃𝑧 𝑥 ∈ 𝑦)) |
44 | 43 | adantll 714 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑧 𝑤 ∈ 𝑦 ↔ ∃𝑧 𝑥 ∈ 𝑦)) |
45 | 12, 34 | nfan1 2202 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥) |
46 | | elequ1 2121 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
47 | 46 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥) → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
48 | 45, 47 | albid 2224 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑥) → (∀𝑦 𝑤 ∈ 𝑧 ↔ ∀𝑦 𝑥 ∈ 𝑧)) |
49 | 48 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦 𝑤 ∈ 𝑧 ↔ ∀𝑦 𝑥 ∈ 𝑧)) |
50 | 44, 49 | imbi12d 348 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧))) |
51 | 50 | ex 416 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧)))) |
52 | 11, 27, 51 | cbvald 2407 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) ↔ ∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧))) |
53 | 52 | adantr 484 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) ↔ ∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧))) |
54 | | elequ2 2129 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
55 | 54 | adantl 485 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
56 | 53, 55 | imbi12d 348 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
57 | 36, 56 | albid 2224 |
. . . . 5
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
58 | 57 | ex 416 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → (∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
59 | 11, 32, 58 | cbvexd 2408 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤∀𝑦(∀𝑤(∃𝑧 𝑤 ∈ 𝑦 → ∀𝑦 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
60 | 8, 59 | mpbii 236 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
61 | 60 | ex 416 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |