Proof of Theorem dvelimor
Step | Hyp | Ref
| Expression |
1 | | ax-bndl 1396 |
. . . . . 6
⊢ (∀x x = z ∨ (∀x x = y ∨ ∀z∀x(z = y →
∀x
z = y))) |
2 | | orcom 646 |
. . . . . . 7
⊢ ((∀x x = y ∨ ∀z∀x(z = y → ∀x z = y)) ↔
(∀z∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
3 | 2 | orbi2i 678 |
. . . . . 6
⊢ ((∀x x = z ∨ (∀x x = y ∨ ∀z∀x(z = y →
∀x
z = y))) ↔ (∀x x = z ∨ (∀z∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
4 | 1, 3 | mpbi 133 |
. . . . 5
⊢ (∀x x = z ∨ (∀z∀x(z = y → ∀x z = y) ∨ ∀x x = y)) |
5 | | orass 683 |
. . . . 5
⊢ (((∀x x = z ∨ ∀z∀x(z = y → ∀x z = y)) ∨ ∀x x = y) ↔ (∀x x = z ∨ (∀z∀x(z = y → ∀x z = y) ∨ ∀x x = y))) |
6 | 4, 5 | mpbir 134 |
. . . 4
⊢ ((∀x x = z ∨ ∀z∀x(z = y → ∀x z = y)) ∨ ∀x x = y) |
7 | | nfae 1604 |
. . . . . . 7
⊢
Ⅎz∀x x = z |
8 | | a16nf 1743 |
. . . . . . 7
⊢ (∀x x = z →
Ⅎx(z = y →
φ)) |
9 | 7, 8 | alrimi 1412 |
. . . . . 6
⊢ (∀x x = z →
∀zℲx(z = y → φ)) |
10 | | df-nf 1347 |
. . . . . . . 8
⊢
(Ⅎx z = y ↔
∀x(z = y → ∀x z = y)) |
11 | | id 19 |
. . . . . . . . 9
⊢
(Ⅎx z = y →
Ⅎx z = y) |
12 | | dvelimor.1 |
. . . . . . . . . 10
⊢
Ⅎxφ |
13 | 12 | a1i 9 |
. . . . . . . . 9
⊢
(Ⅎx z = y →
Ⅎxφ) |
14 | 11, 13 | nfimd 1474 |
. . . . . . . 8
⊢
(Ⅎx z = y →
Ⅎx(z = y →
φ)) |
15 | 10, 14 | sylbir 125 |
. . . . . . 7
⊢ (∀x(z = y →
∀x
z = y)
→ Ⅎx(z = y →
φ)) |
16 | 15 | alimi 1341 |
. . . . . 6
⊢ (∀z∀x(z = y →
∀x
z = y)
→ ∀zℲx(z = y → φ)) |
17 | 9, 16 | jaoi 635 |
. . . . 5
⊢ ((∀x x = z ∨ ∀z∀x(z = y → ∀x z = y)) →
∀zℲx(z = y → φ)) |
18 | 17 | orim1i 676 |
. . . 4
⊢ (((∀x x = z ∨ ∀z∀x(z = y → ∀x z = y)) ∨ ∀x x = y) → (∀zℲx(z = y → φ)
∨ ∀x x = y)) |
19 | 6, 18 | ax-mp 7 |
. . 3
⊢ (∀zℲx(z = y → φ)
∨ ∀x x = y) |
20 | | orcom 646 |
. . 3
⊢ ((∀zℲx(z = y → φ)
∨ ∀x x = y) ↔
(∀x
x = y
∨ ∀zℲx(z = y → φ))) |
21 | 19, 20 | mpbi 133 |
. 2
⊢ (∀x x = y ∨ ∀zℲx(z = y → φ)) |
22 | | nfalt 1467 |
. . . 4
⊢ (∀zℲx(z = y → φ)
→ Ⅎx∀z(z = y →
φ)) |
23 | | ax-17 1416 |
. . . . . 6
⊢ (ψ → ∀zψ) |
24 | | dvelimor.2 |
. . . . . 6
⊢ (z = y →
(φ ↔ ψ)) |
25 | 23, 24 | equsalh 1611 |
. . . . 5
⊢ (∀z(z = y →
φ) ↔ ψ) |
26 | 25 | nfbii 1359 |
. . . 4
⊢
(Ⅎx∀z(z = y →
φ) ↔ Ⅎxψ) |
27 | 22, 26 | sylib 127 |
. . 3
⊢ (∀zℲx(z = y → φ)
→ Ⅎxψ) |
28 | 27 | orim2i 677 |
. 2
⊢ ((∀x x = y ∨ ∀zℲx(z = y → φ))
→ (∀x x = y ∨ Ⅎxψ)) |
29 | 21, 28 | ax-mp 7 |
1
⊢ (∀x x = y ∨ Ⅎxψ) |