Proof of Theorem dvelimfv
Step | Hyp | Ref
| Expression |
1 | | nfnae 1702 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
2 | | ax12or 1488 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) |
3 | | orcom 718 |
. . . . . . . . . 10
⊢
((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)) |
4 | 3 | orbi2i 752 |
. . . . . . . . 9
⊢
((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))) |
5 | 2, 4 | mpbi 144 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)) |
6 | | orass 757 |
. . . . . . . 8
⊢
(((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))) |
7 | 5, 6 | mpbir 145 |
. . . . . . 7
⊢
((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) |
8 | | nfae 1699 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 𝑥 = 𝑧 |
9 | | ax16ALT 1839 |
. . . . . . . . . . 11
⊢
(∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
10 | 8, 9 | nfd 1503 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦) |
11 | | dvelimfv.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥𝜑) |
12 | 11 | nfi 1442 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝜑 |
13 | 12 | a1i 9 |
. . . . . . . . . 10
⊢
(∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑) |
14 | 10, 13 | nfimd 1565 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
15 | | df-nf 1441 |
. . . . . . . . . 10
⊢
(Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) |
16 | | id 19 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) |
17 | 12 | a1i 9 |
. . . . . . . . . . 11
⊢
(Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑) |
18 | 16, 17 | nfimd 1565 |
. . . . . . . . . 10
⊢
(Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
19 | 15, 18 | sylbir 134 |
. . . . . . . . 9
⊢
(∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
20 | 14, 19 | jaoi 706 |
. . . . . . . 8
⊢
((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
21 | 20 | orim1i 750 |
. . . . . . 7
⊢
(((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)) |
22 | 7, 21 | ax-mp 5 |
. . . . . 6
⊢
(Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) |
23 | | orcom 718 |
. . . . . 6
⊢
((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))) |
24 | 22, 23 | mpbi 144 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
25 | 24 | ori 713 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)) |
26 | 1, 25 | nfald 1740 |
. . 3
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑)) |
27 | | dvelimfv.2 |
. . . . 5
⊢ (𝜓 → ∀𝑧𝜓) |
28 | | dvelimfv.3 |
. . . . 5
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) |
29 | 27, 28 | equsalh 1706 |
. . . 4
⊢
(∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓) |
30 | 29 | nfbii 1453 |
. . 3
⊢
(Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓) |
31 | 26, 30 | sylib 121 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) |
32 | 31 | nfrd 1500 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) |