Proof of Theorem dvelimALT
Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . 4
⊢
Ⅎz ¬ ∀x x = y |
2 | | ax-i12 1395 |
. . . . . . . . 9
⊢ (∀x x = z ∨ (∀x x = y ∨ ∀x(z = y →
∀x
z = y))) |
3 | | orcom 646 |
. . . . . . . . . 10
⊢ ((∀x x = y ∨ ∀x(z = y → ∀x z = y)) ↔
(∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
4 | 3 | orbi2i 678 |
. . . . . . . . 9
⊢ ((∀x x = z ∨ (∀x x = y ∨ ∀x(z = y →
∀x
z = y))) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
5 | 2, 4 | mpbi 133 |
. . . . . . . 8
⊢ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
6 | | orass 683 |
. . . . . . . 8
⊢ (((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
7 | 5, 6 | mpbir 134 |
. . . . . . 7
⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) |
8 | | nfa1 1431 |
. . . . . . . . . . 11
⊢
Ⅎx∀x x = z |
9 | | ax16ALT 1736 |
. . . . . . . . . . 11
⊢ (∀x x = z →
(z = y
→ ∀x z = y)) |
10 | 8, 9 | nfd 1413 |
. . . . . . . . . 10
⊢ (∀x x = z →
Ⅎx z = y) |
11 | | dvelimALT.1 |
. . . . . . . . . . . 12
⊢ (φ → ∀xφ) |
12 | 11 | nfi 1348 |
. . . . . . . . . . 11
⊢
Ⅎxφ |
13 | 12 | a1i 9 |
. . . . . . . . . 10
⊢ (∀x x = z →
Ⅎxφ) |
14 | 10, 13 | nfimd 1474 |
. . . . . . . . 9
⊢ (∀x x = z →
Ⅎx(z = y →
φ)) |
15 | | df-nf 1347 |
. . . . . . . . . 10
⊢
(Ⅎx z = y ↔
∀x(z = y → ∀x z = y)) |
16 | | id 19 |
. . . . . . . . . . 11
⊢
(Ⅎx z = y →
Ⅎx z = y) |
17 | 12 | a1i 9 |
. . . . . . . . . . 11
⊢
(Ⅎx z = y →
Ⅎxφ) |
18 | 16, 17 | nfimd 1474 |
. . . . . . . . . 10
⊢
(Ⅎx z = y →
Ⅎx(z = y →
φ)) |
19 | 15, 18 | sylbir 125 |
. . . . . . . . 9
⊢ (∀x(z = y →
∀x
z = y)
→ Ⅎx(z = y →
φ)) |
20 | 14, 19 | jaoi 635 |
. . . . . . . 8
⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) →
Ⅎx(z = y →
φ)) |
21 | 20 | orim1i 676 |
. . . . . . 7
⊢ (((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) → (Ⅎx(z = y → φ)
∨ ∀x x = y)) |
22 | 7, 21 | ax-mp 7 |
. . . . . 6
⊢
(Ⅎx(z = y →
φ) ∨
∀x
x = y) |
23 | | orcom 646 |
. . . . . 6
⊢
((Ⅎx(z = y →
φ) ∨
∀x
x = y)
↔ (∀x x = y ∨ Ⅎx(z = y → φ))) |
24 | 22, 23 | mpbi 133 |
. . . . 5
⊢ (∀x x = y ∨ Ⅎx(z = y → φ)) |
25 | 24 | ori 641 |
. . . 4
⊢ (¬
∀x
x = y
→ Ⅎx(z = y →
φ)) |
26 | 1, 25 | nfald 1640 |
. . 3
⊢ (¬
∀x
x = y
→ Ⅎx∀z(z = y →
φ)) |
27 | | ax-17 1416 |
. . . . 5
⊢ (ψ → ∀zψ) |
28 | | dvelimALT.2 |
. . . . 5
⊢ (z = y →
(φ ↔ ψ)) |
29 | 27, 28 | equsalh 1611 |
. . . 4
⊢ (∀z(z = y →
φ) ↔ ψ) |
30 | 29 | nfbii 1359 |
. . 3
⊢
(Ⅎx∀z(z = y →
φ) ↔ Ⅎxψ) |
31 | 26, 30 | sylib 127 |
. 2
⊢ (¬
∀x
x = y
→ Ⅎxψ) |
32 | 31 | nfrd 1410 |
1
⊢ (¬
∀x
x = y
→ (ψ → ∀xψ)) |