Step | Hyp | Ref
| Expression |
1 | | axunndlem1 9417 |
. . . 4
⊢
∃𝑤∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) |
2 | | nfnae 2318 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
3 | | nfnae 2318 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
4 | 2, 3 | nfan 1828 |
. . . . 5
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
5 | | nfnae 2318 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
6 | | nfnae 2318 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
7 | 5, 6 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
8 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑤(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
9 | | nfcvf 2788 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
10 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦) |
11 | | nfcvd 2765 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤) |
12 | 10, 11 | nfeld 2773 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 ∈ 𝑤) |
13 | | nfcvf 2788 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
14 | 13 | adantl 482 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧) |
15 | 11, 14 | nfeld 2773 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑧) |
16 | 12, 15 | nfand 1826 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧)) |
17 | 8, 16 | nfexd 2167 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧)) |
18 | 17, 12 | nfimd 1823 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
19 | 7, 18 | nfald 2165 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤)) |
20 | | nfcvd 2765 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤) |
21 | | nfcvf2 2789 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥) |
23 | 20, 22 | nfeqd 2772 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥) |
24 | 7, 23 | nfan1 2068 |
. . . . . . 7
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
25 | | elequ2 2004 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
26 | | elequ1 1997 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
27 | 25, 26 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)))) |
29 | 4, 16, 28 | cbvexd 2278 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
30 | 29 | adantr 481 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧))) |
31 | 25 | adantl 482 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥)) |
32 | 30, 31 | imbi12d 334 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
33 | 24, 32 | albid 2090 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
34 | 33 | ex 450 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → (∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) |
35 | 4, 19, 34 | cbvexd 2278 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤∀𝑦(∃𝑤(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧) → 𝑦 ∈ 𝑤) ↔ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
36 | 1, 35 | mpbii 223 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
37 | 36 | ex 450 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) |
38 | | nfae 2316 |
. . . 4
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑦 |
39 | | nfae 2316 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑦 |
40 | | elirrv 8504 |
. . . . . . . . 9
⊢ ¬
𝑦 ∈ 𝑦 |
41 | | elequ2 2004 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
42 | 40, 41 | mtbiri 317 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝑥) |
43 | 42 | intnanrd 963 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
44 | 43 | sps 2055 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
45 | 39, 44 | nexd 2089 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
46 | 45 | pm2.21d 118 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
47 | 38, 46 | alrimi 2082 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
48 | | 19.8a 2052 |
. . 3
⊢
(∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
49 | 47, 48 | syl 17 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
50 | | nfae 2316 |
. . . 4
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑧 |
51 | | nfae 2316 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑧 |
52 | | elirrv 8504 |
. . . . . . . . 9
⊢ ¬
𝑧 ∈ 𝑧 |
53 | | elequ1 1997 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧)) |
54 | 52, 53 | mtbiri 317 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧) |
55 | 54 | intnand 962 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
56 | 55 | sps 2055 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ (𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
57 | 51, 56 | nexd 2089 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → ¬ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧)) |
58 | 57 | pm2.21d 118 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
59 | 50, 58 | alrimi 2082 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → ∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
60 | 59, 48 | syl 17 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) |
61 | 37, 49, 60 | pm2.61ii 177 |
1
⊢
∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) |