Step | Hyp | Ref
| Expression |
1 | | equcomi 2025 |
. . . . 5
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
2 | | axc16 2258 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)) |
3 | 1, 2 | syl5 34 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
4 | 3 | spsd 2184 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
5 | 4 | exlimiv 1938 |
. 2
⊢
(∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
6 | | alnex 1789 |
. . 3
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧) |
7 | | ax6evr 2023 |
. . . . 5
⊢
∃𝑧 𝑥 = 𝑧 |
8 | | 19.29 1881 |
. . . . 5
⊢
((∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧)) |
9 | 7, 8 | mpan2 691 |
. . . 4
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧)) |
10 | | axc9 2381 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))) |
11 | 10 | impcom 411 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) |
12 | | axc11r 2367 |
. . . . . . . . . . 11
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) |
13 | 11, 12 | syl9 77 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))) |
14 | | aev 2063 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) |
15 | 13, 14 | syl8 76 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))) |
16 | 15 | ex 416 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))) |
17 | 16 | com24 95 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))) |
18 | 17 | imp 410 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
19 | | pm2.18 128 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥) |
20 | 18, 19 | syl6 35 |
. . . . 5
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
21 | 20 | exlimiv 1938 |
. . . 4
⊢
(∃𝑧(¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
22 | 9, 21 | syl 17 |
. . 3
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
23 | 6, 22 | sylbir 238 |
. 2
⊢ (¬
∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
24 | 5, 23 | pm2.61i 185 |
1
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |