Step | Hyp | Ref
| Expression |
1 | | axunndlem1 10349 |
. . . 4
⊢
∃𝑤∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) |
2 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
3 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
4 | 2, 3 | nfan 1902 |
. . . . 5
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
5 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
6 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
7 | 5, 6 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
8 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑤(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
9 | | nfcvf 2936 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
10 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦) |
11 | | nfcvd 2908 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤) |
12 | 10, 11 | nfeld 2918 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑤) |
13 | | nfcvf 2936 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
14 | 13 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧) |
15 | 11, 14 | nfeld 2918 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑧) |
16 | 12, 15 | nfand 1900 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧)) |
17 | 8, 16 | nfexd 2323 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧)) |
18 | 17, 12 | nfimd 1897 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
19 | 7, 18 | nfald 2322 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
20 | | nfcvd 2908 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤) |
21 | | nfcvf2 2937 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥) |
23 | 20, 22 | nfeqd 2917 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥) |
24 | 7, 23 | nfan1 2193 |
. . . . . . 7
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
25 | | elequ2 2121 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
26 | | elequ1 2113 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
27 | 25, 26 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)))) |
29 | 4, 16, 28 | cbvexd 2408 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
30 | 29 | adantr 481 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
31 | 25 | adantl 482 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
32 | 30, 31 | imbi12d 345 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
33 | 24, 32 | albid 2215 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
34 | 33 | ex 413 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → (∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
35 | 4, 19, 34 | cbvexd 2408 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
36 | 1, 35 | mpbii 232 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
37 | 36 | ex 413 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
38 | | nfae 2433 |
. . . 4
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑦 |
39 | | nfae 2433 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑦 |
40 | | elirrv 9353 |
. . . . . . . . 9
⊢ ¬
𝑦 ∈ 𝑦 |
41 | | elequ2 2121 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
42 | 40, 41 | mtbiri 327 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝑥) |
43 | 42 | intnanrd 490 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
44 | 43 | sps 2178 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
45 | 39, 44 | nexd 2214 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
46 | 45 | pm2.21d 121 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
47 | 38, 46 | alrimi 2206 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
48 | 47 | 19.8ad 2175 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
49 | | nfae 2433 |
. . . 4
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑧 |
50 | | nfae 2433 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑧 |
51 | | elirrv 9353 |
. . . . . . . . 9
⊢ ¬
𝑧 ∈ 𝑧 |
52 | | elequ1 2113 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧)) |
53 | 51, 52 | mtbiri 327 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧) |
54 | 53 | intnand 489 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
55 | 54 | sps 2178 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
56 | 50, 55 | nexd 2214 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
57 | 56 | pm2.21d 121 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
58 | 49, 57 | alrimi 2206 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
59 | 58 | 19.8ad 2175 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
60 | 37, 48, 59 | pm2.61ii 183 |
1
⊢
∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) |