Step | Hyp | Ref
| Expression |
1 | | zfinf 9397 |
. . . . 5
⊢
∃𝑤(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
2 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
3 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
4 | 2, 3 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
5 | | nfcvf 2936 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦) |
7 | | nfcvd 2908 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤) |
8 | 6, 7 | nfeld 2918 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑤) |
9 | | nfnae 2434 |
. . . . . . . . 9
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
10 | | nfnae 2434 |
. . . . . . . . 9
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
11 | 9, 10 | nfan 1902 |
. . . . . . . 8
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
12 | | nfnae 2434 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
13 | | nfnae 2434 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑧 |
14 | 12, 13 | nfan 1902 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
15 | | nfcvf 2936 |
. . . . . . . . . . . . 13
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
16 | 15 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧) |
17 | 6, 16 | nfeld 2918 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑧) |
18 | 16, 7 | nfeld 2918 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 ∈ 𝑤) |
19 | 17, 18 | nfand 1900 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) |
20 | 14, 19 | nfexd 2323 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) |
21 | 8, 20 | nfimd 1897 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
22 | 11, 21 | nfald 2322 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
23 | 8, 22 | nfand 1900 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))) |
24 | | simpr 485 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → 𝑤 = 𝑥) |
25 | 24 | eleq2d 2824 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
26 | | nfcvd 2908 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤) |
27 | | nfcvf2 2937 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥) |
29 | 26, 28 | nfeqd 2917 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥) |
30 | 11, 29 | nfan1 2193 |
. . . . . . . . 9
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
31 | | nfcvd 2908 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑤) |
32 | | nfcvf2 2937 |
. . . . . . . . . . . . . 14
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥) |
33 | 32 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑥) |
34 | 31, 33 | nfeqd 2917 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥) |
35 | 14, 34 | nfan1 2193 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
36 | | elequ2 2121 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥)) |
37 | 36 | anbi2d 629 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
38 | 37 | adantl 482 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
39 | 35, 38 | exbid 2216 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))) |
40 | 25, 39 | imbi12d 345 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) ↔ (𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
41 | 30, 40 | albid 2215 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
42 | 25, 41 | anbi12d 631 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
43 | 42 | ex 413 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))) |
44 | 4, 23, 43 | cbvexd 2408 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑦 ∈ 𝑤 ∧ ∀𝑦(𝑦 ∈ 𝑤 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
45 | 1, 44 | mpbii 232 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |
46 | 45 | a1d 25 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
47 | 46 | ex 413 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))))) |
48 | | nd1 10343 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑦 ∈ 𝑧) |
49 | 48 | pm2.21d 121 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
50 | | nd2 10344 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑦 ∈ 𝑧) |
51 | 50 | pm2.21d 121 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))) |
52 | 47, 49, 51 | pm2.61ii 183 |
1
⊢
(∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) |