Proof of Theorem bj-nnfalt
Step | Hyp | Ref
| Expression |
1 | | df-bj-nnf 34885 |
. . . 4
⊢
(Ⅎ'𝑦𝜑 ↔ ((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
2 | 1 | albii 1825 |
. . 3
⊢
(∀𝑥Ⅎ'𝑦𝜑 ↔ ∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
3 | | simpl 482 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦𝜑 → 𝜑)) |
4 | 3 | alimi 1817 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(∃𝑦𝜑 → 𝜑)) |
5 | | bj-nnflemea 34926 |
. . . 4
⊢
(∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑)) |
6 | 4, 5 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑)) |
7 | 2, 6 | sylbi 216 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∃𝑦∀𝑥𝜑 → ∀𝑥𝜑)) |
8 | | simpr 484 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (𝜑 → ∀𝑦𝜑)) |
9 | 8 | alimi 1817 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(𝜑 → ∀𝑦𝜑)) |
10 | | bj-nnflemaa 34923 |
. . . 4
⊢
(∀𝑥(𝜑 → ∀𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) |
11 | 9, 10 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) |
12 | 2, 11 | sylbi 216 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)) |
13 | | df-bj-nnf 34885 |
. 2
⊢
(Ⅎ'𝑦∀𝑥𝜑 ↔ ((∃𝑦∀𝑥𝜑 → ∀𝑥𝜑) ∧ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑))) |
14 | 7, 12, 13 | sylanbrc 582 |
1
⊢
(∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∀𝑥𝜑) |