Proof of Theorem hbae
Step | Hyp | Ref
| Expression |
1 | | ax12or 1400 |
. . . 4
⊢ (∀z z = x ∨ (∀z z = y ∨ ∀z(x = y →
∀z
x = y))) |
2 | | ax10o 1600 |
. . . . . 6
⊢ (∀x x = z →
(∀x
x = y
→ ∀z x = y)) |
3 | 2 | alequcoms 1406 |
. . . . 5
⊢ (∀z z = x →
(∀x
x = y
→ ∀z x = y)) |
4 | | ax10o 1600 |
. . . . . . . . 9
⊢ (∀x x = y →
(∀x
x = y
→ ∀y x = y)) |
5 | 4 | pm2.43i 43 |
. . . . . . . 8
⊢ (∀x x = y →
∀y
x = y) |
6 | | ax10o 1600 |
. . . . . . . 8
⊢ (∀y y = z →
(∀y
x = y
→ ∀z x = y)) |
7 | 5, 6 | syl5 28 |
. . . . . . 7
⊢ (∀y y = z →
(∀x
x = y
→ ∀z x = y)) |
8 | 7 | alequcoms 1406 |
. . . . . 6
⊢ (∀z z = y →
(∀x
x = y
→ ∀z x = y)) |
9 | | ax-4 1397 |
. . . . . . . 8
⊢ (∀x x = y →
x = y) |
10 | 9 | imim1i 54 |
. . . . . . 7
⊢
((x = y → ∀z x = y) →
(∀x
x = y
→ ∀z x = y)) |
11 | 10 | sps 1427 |
. . . . . 6
⊢ (∀z(x = y →
∀z
x = y)
→ (∀x x = y → ∀z x = y)) |
12 | 8, 11 | jaoi 635 |
. . . . 5
⊢ ((∀z z = y ∨ ∀z(x = y → ∀z x = y)) →
(∀x
x = y
→ ∀z x = y)) |
13 | 3, 12 | jaoi 635 |
. . . 4
⊢ ((∀z z = x ∨ (∀z z = y ∨ ∀z(x = y →
∀z
x = y))) → (∀x x = y →
∀z
x = y)) |
14 | 1, 13 | ax-mp 7 |
. . 3
⊢ (∀x x = y →
∀z
x = y) |
15 | 14 | a5i 1432 |
. 2
⊢ (∀x x = y →
∀x∀z x = y) |
16 | | ax-7 1334 |
. 2
⊢ (∀x∀z x = y →
∀z∀x x = y) |
17 | 15, 16 | syl 14 |
1
⊢ (∀x x = y →
∀z∀x x = y) |