Step | Hyp | Ref
| Expression |
1 | | sp 2226 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
2 | 1 | con3i 152 |
. 2
⊢ (¬
𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦) |
3 | | p0ex 5084 |
. . . . . . . 8
⊢ {∅}
∈ V |
4 | | eleq2 2896 |
. . . . . . . . . 10
⊢ (𝑥 = {∅} → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ {∅})) |
5 | 4 | imbi2d 332 |
. . . . . . . . 9
⊢ (𝑥 = {∅} → ((𝑤 = ∅ → 𝑤 ∈ 𝑥) ↔ (𝑤 = ∅ → 𝑤 ∈ {∅}))) |
6 | 5 | albidv 2021 |
. . . . . . . 8
⊢ (𝑥 = {∅} →
(∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥) ↔ ∀𝑤(𝑤 = ∅ → 𝑤 ∈ {∅}))) |
7 | 3, 6 | spcev 3518 |
. . . . . . 7
⊢
(∀𝑤(𝑤 = ∅ → 𝑤 ∈ {∅}) →
∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
8 | | 0ex 5015 |
. . . . . . . . 9
⊢ ∅
∈ V |
9 | 8 | snid 4430 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
10 | | eleq1 2895 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 ∈ {∅} ↔ ∅
∈ {∅})) |
11 | 9, 10 | mpbiri 250 |
. . . . . . 7
⊢ (𝑤 = ∅ → 𝑤 ∈
{∅}) |
12 | 7, 11 | mpg 1898 |
. . . . . 6
⊢
∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥) |
13 | | neq0 4160 |
. . . . . . . . . 10
⊢ (¬
𝑤 = ∅ ↔
∃𝑥 𝑥 ∈ 𝑤) |
14 | 13 | con1bii 348 |
. . . . . . . . 9
⊢ (¬
∃𝑥 𝑥 ∈ 𝑤 ↔ 𝑤 = ∅) |
15 | 14 | imbi1i 341 |
. . . . . . . 8
⊢ ((¬
∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
16 | 15 | albii 1920 |
. . . . . . 7
⊢
(∀𝑤(¬
∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
17 | 16 | exbii 1949 |
. . . . . 6
⊢
(∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
18 | 12, 17 | mpbir 223 |
. . . . 5
⊢
∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) |
19 | | nfnae 2456 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
20 | | nfnae 2456 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
21 | | nfcvf2 2995 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
22 | | nfcvd 2971 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
23 | 21, 22 | nfeld 2979 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 ∈ 𝑤) |
24 | 19, 23 | nfexd 2363 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦∃𝑥 𝑥 ∈ 𝑤) |
25 | 24 | nfnd 1960 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 ¬ ∃𝑥 𝑥 ∈ 𝑤) |
26 | 22, 21 | nfeld 2979 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 ∈ 𝑥) |
27 | 25, 26 | nfimd 1998 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥)) |
28 | | nfeqf2 2396 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 = 𝑦) |
29 | 19, 28 | nfan1 2242 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) |
30 | | elequ2 2180 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
31 | 30 | adantl 475 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
32 | 29, 31 | exbid 2268 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (∃𝑥 𝑥 ∈ 𝑤 ↔ ∃𝑥 𝑥 ∈ 𝑦)) |
33 | 32 | notbid 310 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∃𝑥 𝑥 ∈ 𝑤 ↔ ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
34 | | elequ1 2173 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
35 | 34 | adantl 475 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
36 | 33, 35 | imbi12d 336 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
37 | 36 | ex 403 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → ((¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥)))) |
38 | 20, 27, 37 | cbvald 2429 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
39 | 19, 38 | exbid 2268 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
40 | 18, 39 | mpbii 225 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥)) |
41 | | nfae 2454 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑧 |
42 | | nfae 2454 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑧 |
43 | | axc11r 2390 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑥 ¬ 𝑥 ∈ 𝑦)) |
44 | | alnex 1882 |
. . . . . . . . . 10
⊢
(∀𝑧 ¬
𝑥 ∈ 𝑦 ↔ ¬ ∃𝑧 𝑥 ∈ 𝑦) |
45 | | alnex 1882 |
. . . . . . . . . 10
⊢
(∀𝑥 ¬
𝑥 ∈ 𝑦 ↔ ¬ ∃𝑥 𝑥 ∈ 𝑦) |
46 | 43, 44, 45 | 3imtr3g 287 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 → (¬ ∃𝑧 𝑥 ∈ 𝑦 → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
47 | | nd3 9727 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑦 𝑥 ∈ 𝑧) |
48 | 47 | pm2.21d 119 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑦 𝑥 ∈ 𝑧 → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
49 | 46, 48 | jad 176 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑧 → ((∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
50 | 49 | spsd 2230 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
51 | 50 | imim1d 82 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → ((¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
52 | 42, 51 | alimd 2257 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → ∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
53 | 41, 52 | eximd 2261 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
54 | 40, 53 | syl5com 31 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
55 | | axpowndlem2 9736 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
56 | 54, 55 | pm2.61d 172 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
57 | 2, 56 | syl 17 |
1
⊢ (¬
𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |