| Step | Hyp | Ref
| Expression |
| 1 | | equcomi 2016 |
. . . . 5
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
| 2 | | axc16 2261 |
. . . . 5
⊢
(∀𝑦 𝑦 = 𝑧 → (𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)) |
| 3 | 1, 2 | syl5 34 |
. . . 4
⊢
(∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 4 | 3 | spsd 2187 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 5 | 4 | exlimiv 1930 |
. 2
⊢
(∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 6 | | alnex 1781 |
. . 3
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 ↔ ¬ ∃𝑧∀𝑦 𝑦 = 𝑧) |
| 7 | | ax6evr 2014 |
. . . . 5
⊢
∃𝑧 𝑥 = 𝑧 |
| 8 | | 19.29 1873 |
. . . . 5
⊢
((∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 ∧ ∃𝑧 𝑥 = 𝑧) → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧)) |
| 9 | 7, 8 | mpan2 691 |
. . . 4
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 → ∃𝑧(¬ ∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧)) |
| 10 | | axc9 2387 |
. . . . . . . . . . . 12
⊢ (¬
∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧))) |
| 11 | 10 | impcom 407 |
. . . . . . . . . . 11
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (𝑥 = 𝑧 → ∀𝑦 𝑥 = 𝑧)) |
| 12 | | axc11r 2371 |
. . . . . . . . . . 11
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧)) |
| 13 | 11, 12 | syl9 77 |
. . . . . . . . . 10
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑥 𝑥 = 𝑧))) |
| 14 | | aev 2057 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥) |
| 15 | 13, 14 | syl8 76 |
. . . . . . . . 9
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥))) |
| 16 | 15 | ex 412 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑥)))) |
| 17 | 16 | com24 95 |
. . . . . . 7
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥)))) |
| 18 | 17 | imp 406 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥))) |
| 19 | | pm2.18 128 |
. . . . . 6
⊢ ((¬
∀𝑦 𝑦 = 𝑥 → ∀𝑦 𝑦 = 𝑥) → ∀𝑦 𝑦 = 𝑥) |
| 20 | 18, 19 | syl6 35 |
. . . . 5
⊢ ((¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 21 | 20 | exlimiv 1930 |
. . . 4
⊢
(∃𝑧(¬
∀𝑦 𝑦 = 𝑧 ∧ 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 22 | 9, 21 | syl 17 |
. . 3
⊢
(∀𝑧 ¬
∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 23 | 6, 22 | sylbir 235 |
. 2
⊢ (¬
∃𝑧∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)) |
| 24 | 5, 23 | pm2.61i 182 |
1
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |