Step | Hyp | Ref
| Expression |
1 | | axrepndlem1 10092 |
. . 3
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∃𝑤(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))) |
2 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
3 | | nfnae 2434 |
. . . . 5
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑧 |
4 | 2, 3 | nfan 1906 |
. . . 4
⊢
Ⅎ𝑥(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
5 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
6 | | nfnae 2434 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑧 |
7 | 5, 6 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑦(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
8 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
9 | | nfnae 2434 |
. . . . . . . 8
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑧 |
10 | 8, 9 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑧(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
11 | | nfs1v 2161 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥[𝑤 / 𝑥]𝜑) |
13 | | nfcvf 2928 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝑧) |
14 | 13 | adantl 485 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑧) |
15 | | nfcvf 2928 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
16 | 15 | adantr 484 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑦) |
17 | 14, 16 | nfeqd 2909 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 = 𝑦) |
18 | 12, 17 | nfimd 1901 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦)) |
19 | 10, 18 | nfald 2330 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦)) |
20 | 7, 19 | nfexd 2331 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦)) |
21 | | nfcvd 2900 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥𝑤) |
22 | 14, 21 | nfeld 2910 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑧 ∈ 𝑤) |
23 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑤(¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) |
24 | 21, 16 | nfeld 2910 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 ∈ 𝑦) |
25 | 7, 12 | nfald 2330 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑦[𝑤 / 𝑥]𝜑) |
26 | 24, 25 | nfand 1904 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) |
27 | 23, 26 | nfexd 2331 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) |
28 | 22, 27 | nfbid 1909 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) |
29 | 10, 28 | nfald 2330 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) |
30 | 20, 29 | nfimd 1901 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)))) |
31 | | nfcvd 2900 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑤) |
32 | | nfcvf2 2929 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
33 | 32 | adantr 484 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦𝑥) |
34 | 31, 33 | nfeqd 2909 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑦 𝑤 = 𝑥) |
35 | 7, 34 | nfan1 2202 |
. . . . . . 7
⊢
Ⅎ𝑦((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
36 | | nfcvd 2900 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑤) |
37 | | nfcvf2 2929 |
. . . . . . . . . . 11
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧𝑥) |
38 | 37 | adantl 485 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧𝑥) |
39 | 36, 38 | nfeqd 2909 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑥) |
40 | 10, 39 | nfan1 2202 |
. . . . . . . 8
⊢
Ⅎ𝑧((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) |
41 | | sbequ12r 2254 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑)) |
42 | 41 | imbi1d 345 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))) |
43 | 42 | adantl 485 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ (𝜑 → 𝑧 = 𝑦))) |
44 | 40, 43 | albid 2224 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ ∀𝑧(𝜑 → 𝑧 = 𝑦))) |
45 | 35, 44 | exbid 2225 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦))) |
46 | | elequ2 2129 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥)) |
47 | 46 | adantl 485 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑥)) |
48 | | elequ1 2121 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
49 | 48 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦)) |
50 | 41 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ([𝑤 / 𝑥]𝜑 ↔ 𝜑)) |
51 | 35, 50 | albid 2224 |
. . . . . . . . . . . 12
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑦[𝑤 / 𝑥]𝜑 ↔ ∀𝑦𝜑)) |
52 | 49, 51 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
53 | 52 | ex 416 |
. . . . . . . . . 10
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ (𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
54 | 4, 26, 53 | cbvexd 2408 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
55 | 54 | adantr 484 |
. . . . . . . 8
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑) ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) |
56 | 47, 55 | bibi12d 349 |
. . . . . . 7
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ (𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
57 | 40, 56 | albid 2224 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → (∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |
58 | 45, 57 | imbi12d 348 |
. . . . 5
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑥) → ((∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
59 | 58 | ex 416 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (𝑤 = 𝑥 → ((∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ (∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))))) |
60 | 4, 30, 59 | cbvexd 2408 |
. . 3
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∃𝑤(∃𝑦∀𝑧([𝑤 / 𝑥]𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑤 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ ∀𝑦[𝑤 / 𝑥]𝜑))) ↔ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
61 | 1, 60 | syl5ib 247 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))) |
62 | 61 | imp 410 |
1
⊢ (((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) |