Proof of Theorem hbae
Step | Hyp | Ref
| Expression |
1 | | ax12or 1501 |
. . . 4
⊢
(∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
2 | | ax10o 1708 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
3 | 2 | alequcoms 1509 |
. . . . 5
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
4 | | ax10o 1708 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦)) |
5 | 4 | pm2.43i 49 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑥 = 𝑦) |
6 | | ax10o 1708 |
. . . . . . . 8
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑦 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
7 | 5, 6 | syl5 32 |
. . . . . . 7
⊢
(∀𝑦 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
8 | 7 | alequcoms 1509 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑦 → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
9 | | ax-4 1503 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
10 | 9 | imim1i 60 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
11 | 10 | sps 1530 |
. . . . . 6
⊢
(∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
12 | 8, 11 | jaoi 711 |
. . . . 5
⊢
((∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
13 | 3, 12 | jaoi 711 |
. . . 4
⊢
((∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) → (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
14 | 1, 13 | ax-mp 5 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦) |
15 | 14 | a5i 1536 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑧 𝑥 = 𝑦) |
16 | | ax-7 1441 |
. 2
⊢
(∀𝑥∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) |
17 | 15, 16 | syl 14 |
1
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) |