Proof of Theorem wl-nfeqfb
Step | Hyp | Ref
| Expression |
1 | | nf5r 2191 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
2 | 1 | imp 407 |
. . . 4
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧) → ∀𝑥 𝑦 = 𝑧) |
3 | | wl-aleq 35690 |
. . . . 5
⊢
(∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) |
4 | 3 | simprbi 497 |
. . . 4
⊢
(∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
5 | 2, 4 | syl 17 |
. . 3
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
6 | | nfnt 1863 |
. . . . . 6
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → Ⅎ𝑥 ¬ 𝑦 = 𝑧) |
7 | 6 | nf5rd 2193 |
. . . . 5
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 → ∀𝑥 ¬ 𝑦 = 𝑧)) |
8 | 7 | imp 407 |
. . . 4
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → ∀𝑥 ¬ 𝑦 = 𝑧) |
9 | | alnex 1788 |
. . . . . 6
⊢
(∀𝑥 ¬
𝑦 = 𝑧 ↔ ¬ ∃𝑥 𝑦 = 𝑧) |
10 | | wl-exeq 35689 |
. . . . . 6
⊢
(∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |
11 | 9, 10 | xchbinx 334 |
. . . . 5
⊢
(∀𝑥 ¬
𝑦 = 𝑧 ↔ ¬ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) |
12 | | 3ioran 1105 |
. . . . 5
⊢ (¬
(𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧) ↔ (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
13 | 11, 12 | sylbb 218 |
. . . 4
⊢
(∀𝑥 ¬
𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
14 | | 3simpc 1149 |
. . . 4
⊢ ((¬
𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)) |
15 | | pm5.21 822 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
16 | 8, 13, 14, 15 | 4syl 19 |
. . 3
⊢
((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
17 | 5, 16 | pm2.61dan 810 |
. 2
⊢
(Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |
18 | | ax7 2023 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) |
19 | 18 | al2imi 1822 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
20 | | nftht 1799 |
. . . 4
⊢
(∀𝑥 𝑦 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧) |
21 | 19, 20 | syl6 35 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧)) |
22 | | nfeqf 2383 |
. . . 4
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧) |
23 | 22 | ex 413 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧)) |
24 | 21, 23 | bija 382 |
. 2
⊢
((∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧) |
25 | 17, 24 | impbii 208 |
1
⊢
(Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) |