Proof of Theorem dveeq2
Step | Hyp | Ref
| Expression |
1 | | ax-i12 1395 |
. . . . 5
⊢ (∀x x = z ∨ (∀x x = y ∨ ∀x(z = y →
∀x
z = y))) |
2 | | orcom 646 |
. . . . . 6
⊢ ((∀x x = y ∨ ∀x(z = y → ∀x z = y)) ↔
(∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
3 | 2 | orbi2i 678 |
. . . . 5
⊢ ((∀x x = z ∨ (∀x x = y ∨ ∀x(z = y →
∀x
z = y))) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
4 | 1, 3 | mpbi 133 |
. . . 4
⊢ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
5 | | orass 683 |
. . . 4
⊢ (((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
6 | 4, 5 | mpbir 134 |
. . 3
⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) |
7 | | orel2 644 |
. . 3
⊢ (¬
∀x
x = y
→ (((∀x x = z ∨ ∀x(z = y →
∀x
z = y))
∨ ∀x x = y) →
(∀x
x = z
∨ ∀x(z = y →
∀x
z = y)))) |
8 | 6, 7 | mpi 15 |
. 2
⊢ (¬
∀x
x = y
→ (∀x x = z ∨ ∀x(z = y →
∀x
z = y))) |
9 | | ax16 1691 |
. . 3
⊢ (∀x x = z →
(z = y
→ ∀x z = y)) |
10 | | sp 1398 |
. . 3
⊢ (∀x(z = y →
∀x
z = y)
→ (z = y → ∀x z = y)) |
11 | 9, 10 | jaoi 635 |
. 2
⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) →
(z = y
→ ∀x z = y)) |
12 | 8, 11 | syl 14 |
1
⊢ (¬
∀x
x = y
→ (z = y → ∀x z = y)) |