Step | Hyp | Ref
| Expression |
1 | | zfac 10214 |
. . . 4
⊢
∃𝑣∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) |
2 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
3 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
4 | | nfnae 2434 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑤 |
5 | 2, 3, 4 | nf3an 1904 |
. . . . 5
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) |
6 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
7 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
8 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑤 |
9 | 6, 7, 8 | nf3an 1904 |
. . . . . 6
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) |
10 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑧 |
11 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
12 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑤 |
13 | 10, 11, 12 | nf3an 1904 |
. . . . . . 7
⊢
Ⅎ𝑧(¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) |
14 | | nfcvf 2936 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
15 | 14 | 3ad2ant2 1133 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑦) |
16 | | nfcvf 2936 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
17 | 16 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑧) |
18 | 15, 17 | nfeld 2918 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 ∈ 𝑧) |
19 | | nfcvf 2936 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑤 → Ⅎ𝑥𝑤) |
20 | 19 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑤) |
21 | 17, 20 | nfeld 2918 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑧 ∈ 𝑤) |
22 | 18, 21 | nfand 1900 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) |
23 | | nfnae 2434 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 ¬
∀𝑥 𝑥 = 𝑧 |
24 | | nfnae 2434 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 ¬
∀𝑥 𝑥 = 𝑦 |
25 | | nfnae 2434 |
. . . . . . . . . 10
⊢
Ⅎ𝑤 ¬
∀𝑥 𝑥 = 𝑤 |
26 | 23, 24, 25 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑤(¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) |
27 | 15, 20 | nfeld 2918 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 ∈ 𝑤) |
28 | | nfcvd 2908 |
. . . . . . . . . . . . . . 15
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥𝑣) |
29 | 20, 28 | nfeld 2918 |
. . . . . . . . . . . . . 14
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑤 ∈ 𝑣) |
30 | 27, 29 | nfand 1900 |
. . . . . . . . . . . . 13
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) |
31 | 22, 30 | nfand 1900 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣))) |
32 | 26, 31 | nfexd 2323 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣))) |
33 | 15, 20 | nfeqd 2917 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥 𝑦 = 𝑤) |
34 | 32, 33 | nfbid 1905 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) |
35 | 9, 34 | nfald 2322 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) |
36 | 26, 35 | nfexd 2323 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) |
37 | 22, 36 | nfimd 1897 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))) |
38 | 13, 37 | nfald 2322 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))) |
39 | 9, 38 | nfald 2322 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑥∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤))) |
40 | | nfcvd 2908 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦𝑣) |
41 | | nfcvf2 2937 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
42 | 41 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦𝑥) |
43 | 40, 42 | nfeqd 2917 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑥) |
44 | 9, 43 | nfan1 2193 |
. . . . . . 7
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) |
45 | | nfcvd 2908 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧𝑣) |
46 | | nfcvf2 2937 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥) |
47 | 46 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧𝑥) |
48 | 45, 47 | nfeqd 2917 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑧 𝑣 = 𝑥) |
49 | 13, 48 | nfan1 2193 |
. . . . . . . 8
⊢
Ⅎ𝑧((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) |
50 | 22 | nf5rd 2189 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
51 | 50 | adantr 481 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
52 | | sp 2176 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)) |
53 | 51, 52 | impbid1 224 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ↔ ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤))) |
54 | | nfcvd 2908 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤𝑣) |
55 | | nfcvf2 2937 |
. . . . . . . . . . . . 13
⊢ (¬
∀𝑥 𝑥 = 𝑤 → Ⅎ𝑤𝑥) |
56 | 55 | 3ad2ant3 1134 |
. . . . . . . . . . . 12
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤𝑥) |
57 | 54, 56 | nfeqd 2917 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑥) |
58 | 26, 57 | nfan1 2193 |
. . . . . . . . . 10
⊢
Ⅎ𝑤((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) |
59 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → 𝑣 = 𝑥) |
60 | 59 | eleq2d 2824 |
. . . . . . . . . . . . . . 15
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (𝑤 ∈ 𝑣 ↔ 𝑤 ∈ 𝑥)) |
61 | 60 | anbi2d 629 |
. . . . . . . . . . . . . 14
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣) ↔ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))) |
62 | 61 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))) |
63 | 58, 62 | exbid 2216 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))) |
64 | 63 | bibi1d 344 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → ((∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
65 | 44, 64 | albid 2215 |
. . . . . . . . . 10
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
66 | 58, 65 | exbid 2216 |
. . . . . . . . 9
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
67 | 53, 66 | imbi12d 345 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))) |
68 | 49, 67 | albid 2215 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))) |
69 | 44, 68 | albid 2215 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ 𝑣 = 𝑥) → (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))) |
70 | 69 | ex 413 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑥 → (∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))) |
71 | 5, 39, 70 | cbvexd 2408 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑣)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))) |
72 | 1, 71 | mpbii 232 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
73 | 72 | 3exp 1118 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))) |
74 | | axacndlem2 10362 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
75 | | axacndlem1 10361 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
76 | | nfae 2433 |
. . . 4
⊢
Ⅎ𝑦∀𝑥 𝑥 = 𝑤 |
77 | | nfae 2433 |
. . . . 5
⊢
Ⅎ𝑧∀𝑥 𝑥 = 𝑤 |
78 | | simpr 485 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → 𝑧 ∈ 𝑤) |
79 | 78 | alimi 1814 |
. . . . . 6
⊢
(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥 𝑧 ∈ 𝑤) |
80 | | nd2 10342 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑤 → ¬ ∀𝑥 𝑧 ∈ 𝑤) |
81 | 80 | pm2.21d 121 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑤 → (∀𝑥 𝑧 ∈ 𝑤 → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
82 | 79, 81 | syl5 34 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
83 | 77, 82 | alrimi 2206 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑤 → ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
84 | 76, 83 | alrimi 2206 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑤 → ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
85 | 84 | 19.8ad 2175 |
. 2
⊢
(∀𝑥 𝑥 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) |
86 | 73, 74, 75, 85 | pm2.61iii 185 |
1
⊢
∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) |