Proof of Theorem bj-nnfext
| Step | Hyp | Ref
| Expression |
| 1 | | df-bj-nnf 36725 |
. . . 4
⊢
(Ⅎ'𝑦𝜑 ↔ ((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
| 2 | 1 | albii 1819 |
. . 3
⊢
(∀𝑥Ⅎ'𝑦𝜑 ↔ ∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑))) |
| 3 | | simpl 482 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦𝜑 → 𝜑)) |
| 4 | 3 | alimi 1811 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(∃𝑦𝜑 → 𝜑)) |
| 5 | | bj-nnflemee 36764 |
. . . 4
⊢
(∀𝑥(∃𝑦𝜑 → 𝜑) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
| 6 | 4, 5 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
| 7 | 2, 6 | sylbi 217 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∃𝑦∃𝑥𝜑 → ∃𝑥𝜑)) |
| 8 | | simpr 484 |
. . . . 5
⊢
(((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (𝜑 → ∀𝑦𝜑)) |
| 9 | 8 | alimi 1811 |
. . . 4
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → ∀𝑥(𝜑 → ∀𝑦𝜑)) |
| 10 | | bj-nnflemae 36765 |
. . . 4
⊢
(∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
| 11 | 9, 10 | syl 17 |
. . 3
⊢
(∀𝑥((∃𝑦𝜑 → 𝜑) ∧ (𝜑 → ∀𝑦𝜑)) → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
| 12 | 2, 11 | sylbi 217 |
. 2
⊢
(∀𝑥Ⅎ'𝑦𝜑 → (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑)) |
| 13 | | df-bj-nnf 36725 |
. 2
⊢
(Ⅎ'𝑦∃𝑥𝜑 ↔ ((∃𝑦∃𝑥𝜑 → ∃𝑥𝜑) ∧ (∃𝑥𝜑 → ∀𝑦∃𝑥𝜑))) |
| 14 | 7, 12, 13 | sylanbrc 583 |
1
⊢
(∀𝑥Ⅎ'𝑦𝜑 → Ⅎ'𝑦∃𝑥𝜑) |