Proof of Theorem ax12v2-o
Step | Hyp | Ref
| Expression |
1 | | ax6ev 1877 |
. 2
⊢
∃𝑧 𝑧 = 𝑦 |
2 | | ax12v2-o.1 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) |
3 | | equequ2 1940 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
5 | | dveeq2-o 33236 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
6 | 5 | imp 444 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ∀𝑥 𝑧 = 𝑦) |
7 | | nfa1-o 33218 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 𝑧 = 𝑦 |
8 | 3 | imbi1d 330 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))) |
9 | 8 | sps-o 33211 |
. . . . . . . . 9
⊢
(∀𝑥 𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ↔ (𝑥 = 𝑦 → 𝜑))) |
10 | 7, 9 | albid 2077 |
. . . . . . . 8
⊢
(∀𝑥 𝑧 = 𝑦 → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (∀𝑥(𝑥 = 𝑧 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
12 | 11 | imbi2d 329 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ((𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
13 | 4, 12 | imbi12d 333 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → ((𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ↔ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
14 | 2, 13 | mpbii 222 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑧 = 𝑦) → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
15 | 14 | ex 449 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
16 | 15 | exlimdv 1848 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))) |
17 | 1, 16 | mpi 20 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |