Proof of Theorem wl-nfeqfb
Step | Hyp | Ref
| Expression |
1 | | nf5r 2183 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
2 | 1 | imp 405 |
. . . 4
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧) → ∀𝑥 𝑦 = 𝑧) |
3 | | wl-aleq 37232 |
. . . . 5
⊢
(∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) |
4 | 3 | simprbi 495 |
. . . 4
⊢
(∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
5 | 2, 4 | syl 17 |
. . 3
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
6 | | nfnt 1852 |
. . . . . 6
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → Ⅎ𝑥 ¬ 𝑦 = 𝑧) |
7 | 6 | nf5rd 2185 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 → ∀𝑥 ¬ 𝑦 = 𝑧)) |
8 | 7 | imp 405 |
. . . 4
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → ∀𝑥 ¬ 𝑦 = 𝑧) |
9 | | alnex 1776 |
. . . . . 6
⊢
(∀𝑥 ¬
𝑦 = 𝑧 ↔ ¬ ∃𝑥 𝑦 = 𝑧) |
10 | | wl-exeq 37231 |
. . . . . 6
⊢
(∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |
11 | 9, 10 | xchbinx 333 |
. . . . 5
⊢
(∀𝑥 ¬
𝑦 = 𝑧 ↔ ¬ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |
12 | | 3ioran 1103 |
. . . . 5
⊢ (¬
(𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧) ↔ (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
13 | 11, 12 | sylbb 218 |
. . . 4
⊢
(∀𝑥 ¬
𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
14 | | 3simpc 1147 |
. . . 4
⊢ ((¬
𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
15 | | pm5.21 823 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
16 | 8, 13, 14, 15 | 4syl 19 |
. . 3
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
17 | 5, 16 | pm2.61dan 811 |
. 2
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
18 | | ax7 2012 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
19 | 18 | al2imi 1810 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
20 | | nftht 1787 |
. . . 4
⊢
(∀𝑥 𝑦 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧) |
21 | 19, 20 | syl6 35 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧)) |
22 | | nfeqf 2375 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧) |
23 | 22 | ex 411 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧)) |
24 | 21, 23 | bija 379 |
. 2
⊢
((∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧) |
25 | 17, 24 | impbii 208 |
1
⊢
(Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |