Step | Hyp | Ref
| Expression |
1 | | sp 2180 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
2 | | p0ex 5250 |
. . . . . . . 8
⊢ {∅}
∈ V |
3 | | eleq2 2878 |
. . . . . . . . . 10
⊢ (𝑥 = {∅} → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ {∅})) |
4 | 3 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑥 = {∅} → ((𝑤 = ∅ → 𝑤 ∈ 𝑥) ↔ (𝑤 = ∅ → 𝑤 ∈ {∅}))) |
5 | 4 | albidv 1921 |
. . . . . . . 8
⊢ (𝑥 = {∅} →
(∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥) ↔ ∀𝑤(𝑤 = ∅ → 𝑤 ∈ {∅}))) |
6 | 2, 5 | spcev 3555 |
. . . . . . 7
⊢
(∀𝑤(𝑤 = ∅ → 𝑤 ∈ {∅}) →
∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
7 | | 0ex 5175 |
. . . . . . . . 9
⊢ ∅
∈ V |
8 | 7 | snid 4561 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
9 | | eleq1 2877 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑤 ∈ {∅} ↔ ∅
∈ {∅})) |
10 | 8, 9 | mpbiri 261 |
. . . . . . 7
⊢ (𝑤 = ∅ → 𝑤 ∈
{∅}) |
11 | 6, 10 | mpg 1799 |
. . . . . 6
⊢
∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥) |
12 | | neq0 4259 |
. . . . . . . . . 10
⊢ (¬
𝑤 = ∅ ↔
∃𝑥 𝑥 ∈ 𝑤) |
13 | 12 | con1bii 360 |
. . . . . . . . 9
⊢ (¬
∃𝑥 𝑥 ∈ 𝑤 ↔ 𝑤 = ∅) |
14 | 13 | imbi1i 353 |
. . . . . . . 8
⊢ ((¬
∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
15 | 14 | albii 1821 |
. . . . . . 7
⊢
(∀𝑤(¬
∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
16 | 15 | exbii 1849 |
. . . . . 6
⊢
(∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑤(𝑤 = ∅ → 𝑤 ∈ 𝑥)) |
17 | 11, 16 | mpbir 234 |
. . . . 5
⊢
∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) |
18 | | nfnae 2445 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
19 | | nfnae 2445 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
20 | | nfcvf2 2982 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
21 | | nfcvd 2956 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
22 | 20, 21 | nfeld 2966 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 ∈ 𝑤) |
23 | 18, 22 | nfexd 2337 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦∃𝑥 𝑥 ∈ 𝑤) |
24 | 23 | nfnd 1859 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 ¬ ∃𝑥 𝑥 ∈ 𝑤) |
25 | 21, 20 | nfeld 2966 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 ∈ 𝑥) |
26 | 24, 25 | nfimd 1895 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥)) |
27 | | nfeqf2 2384 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 = 𝑦) |
28 | 18, 27 | nfan1 2198 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) |
29 | | elequ2 2126 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
30 | 29 | adantl 485 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦)) |
31 | 28, 30 | exbid 2223 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (∃𝑥 𝑥 ∈ 𝑤 ↔ ∃𝑥 𝑥 ∈ 𝑦)) |
32 | 31 | notbid 321 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (¬ ∃𝑥 𝑥 ∈ 𝑤 ↔ ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
33 | | elequ1 2118 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
34 | 33 | adantl 485 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → (𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
35 | 32, 34 | imbi12d 348 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦) → ((¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
36 | 35 | ex 416 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑤 = 𝑦 → ((¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ (¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥)))) |
37 | 19, 26, 36 | cbvald 2417 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
38 | 18, 37 | exbid 2223 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∀𝑤(¬ ∃𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥) ↔ ∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥))) |
39 | 17, 38 | mpbii 236 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥)) |
40 | | nfae 2444 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑧 |
41 | | nfae 2444 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑧 |
42 | | axc11r 2375 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑥 ¬ 𝑥 ∈ 𝑦)) |
43 | | alnex 1783 |
. . . . . . . . . 10
⊢
(∀𝑧 ¬
𝑥 ∈ 𝑦 ↔ ¬ ∃𝑧 𝑥 ∈ 𝑦) |
44 | | alnex 1783 |
. . . . . . . . . 10
⊢
(∀𝑥 ¬
𝑥 ∈ 𝑦 ↔ ¬ ∃𝑥 𝑥 ∈ 𝑦) |
45 | 42, 43, 44 | 3imtr3g 298 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 → (¬ ∃𝑧 𝑥 ∈ 𝑦 → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
46 | | nd3 10000 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑦 𝑥 ∈ 𝑧) |
47 | 46 | pm2.21d 121 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑦 𝑥 ∈ 𝑧 → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
48 | 45, 47 | jad 190 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑧 → ((∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
49 | 48 | spsd 2184 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → ¬ ∃𝑥 𝑥 ∈ 𝑦)) |
50 | 49 | imim1d 82 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → ((¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → (∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
51 | 41, 50 | alimd 2210 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → ∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
52 | 40, 51 | eximd 2214 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥∀𝑦(¬ ∃𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥) → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
53 | 39, 52 | syl5com 31 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
54 | | axpowndlem2 10009 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
55 | 53, 54 | pm2.61d 182 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
56 | 1, 55 | nsyl5 162 |
1
⊢ (¬
𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |