Proof of Theorem moexex
Step | Hyp | Ref
| Expression |
1 | | nfmo1 2469 |
. . . 4
⊢
Ⅎ𝑥∃*𝑥𝜑 |
2 | | nfa1 2015 |
. . . . 5
⊢
Ⅎ𝑥∀𝑥∃*𝑦𝜓 |
3 | | nfe1 2014 |
. . . . . 6
⊢
Ⅎ𝑥∃𝑥(𝜑 ∧ 𝜓) |
4 | 3 | nfmo 2475 |
. . . . 5
⊢
Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓) |
5 | 2, 4 | nfim 1813 |
. . . 4
⊢
Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
6 | | moexex.1 |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
7 | 6 | nfmo 2475 |
. . . . . 6
⊢
Ⅎ𝑦∃*𝑥𝜑 |
8 | | mopick 2523 |
. . . . . . . 8
⊢
((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) |
9 | 8 | ex 449 |
. . . . . . 7
⊢
(∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓))) |
10 | 9 | com23 84 |
. . . . . 6
⊢
(∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
11 | 7, 6, 10 | alrimd 2071 |
. . . . 5
⊢
(∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
12 | | moim 2507 |
. . . . . 6
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
13 | 12 | spsd 2045 |
. . . . 5
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
14 | 11, 13 | syl6 34 |
. . . 4
⊢
(∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
15 | 1, 5, 14 | exlimd 2074 |
. . 3
⊢
(∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
16 | 6 | nfex 2140 |
. . . . . . 7
⊢
Ⅎ𝑦∃𝑥𝜑 |
17 | | exsimpl 1783 |
. . . . . . 7
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
18 | 16, 17 | exlimi 2073 |
. . . . . 6
⊢
(∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
19 | | exmo 2483 |
. . . . . . 7
⊢
(∃𝑦∃𝑥(𝜑 ∧ 𝜓) ∨ ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
20 | 19 | ori 389 |
. . . . . 6
⊢ (¬
∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
21 | 18, 20 | nsyl4 155 |
. . . . 5
⊢ (¬
∃*𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
22 | 21 | con1i 143 |
. . . 4
⊢ (¬
∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
23 | 22 | a1d 25 |
. . 3
⊢ (¬
∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
24 | 15, 23 | pm2.61d1 170 |
. 2
⊢
(∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
25 | 24 | imp 444 |
1
⊢
((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |