Proof of Theorem bj-nnfext
Step | Hyp | Ref
| Expression |
1 | | df-bj-nnf 34906 |
. . . 4
⊢
(Ⅎ'𝑦𝜑 ↔ ((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
2 | 1 | albii 1822 |
. . 3
⊢
(∀𝑥Ⅎ'𝑦𝜑 ↔ ∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
3 | | simpl 483 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦𝜑 → 𝜑)) |
4 | 3 | alimi 1814 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(∃𝑦𝜑 → 𝜑)) |
5 | | bj-nnflemee 34945 |
. . . 4
⊢
(∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
6 | 4, 5 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
7 | 2, 6 | sylbi 216 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
8 | | simpr 485 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (𝜑 → ∀𝑦𝜑)) |
9 | 8 | alimi 1814 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(𝜑 → ∀𝑦𝜑)) |
10 | | bj-nnflemae 34946 |
. . . 4
⊢
(∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
11 | 9, 10 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
12 | 2, 11 | sylbi 216 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
13 | | df-bj-nnf 34906 |
. 2
⊢
(Ⅎ'𝑦∃𝑥𝜑 ↔ ((∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) ∧ (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑))) |
14 | 7, 12, 13 | sylanbrc 583 |
1
⊢
(∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) |