Proof of Theorem moexexdc
Step | Hyp | Ref
| Expression |
1 | | df-dc 821 |
. 2
⊢
(DECID ∃𝑥𝜑 ↔ (∃𝑥𝜑 ∨ ¬ ∃𝑥𝜑)) |
2 | | hbmo1 2044 |
. . . . . 6
⊢
(∃*𝑥𝜑 → ∀𝑥∃*𝑥𝜑) |
3 | | hba1 1520 |
. . . . . . 7
⊢
(∀𝑥∃*𝑦𝜓 → ∀𝑥∀𝑥∃*𝑦𝜓) |
4 | | hbe1 1475 |
. . . . . . . 8
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∀𝑥∃𝑥(𝜑 ∧ 𝜓)) |
5 | 4 | hbmo 2045 |
. . . . . . 7
⊢
(∃*𝑦∃𝑥(𝜑 ∧ 𝜓) → ∀𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
6 | 3, 5 | hbim 1525 |
. . . . . 6
⊢
((∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) → ∀𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
7 | 2, 6 | hbim 1525 |
. . . . 5
⊢
((∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) → ∀𝑥(∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
8 | | moexexdc.1 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
9 | 8 | nfri 1499 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦𝜑) |
10 | 9 | hbmo 2045 |
. . . . . . 7
⊢
(∃*𝑥𝜑 → ∀𝑦∃*𝑥𝜑) |
11 | | mopick 2084 |
. . . . . . . . 9
⊢
((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) |
12 | 11 | ex 114 |
. . . . . . . 8
⊢
(∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓))) |
13 | 12 | com3r 79 |
. . . . . . 7
⊢ (𝜑 → (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
14 | 9, 10, 13 | alrimdh 1459 |
. . . . . 6
⊢ (𝜑 → (∃*𝑥𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
15 | | moim 2070 |
. . . . . . 7
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
16 | 15 | spsd 1518 |
. . . . . 6
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
17 | 14, 16 | syl6 33 |
. . . . 5
⊢ (𝜑 → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
18 | 7, 17 | exlimih 1573 |
. . . 4
⊢
(∃𝑥𝜑 → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
19 | 9 | hbex 1616 |
. . . . . . . . 9
⊢
(∃𝑥𝜑 → ∀𝑦∃𝑥𝜑) |
20 | | exsimpl 1597 |
. . . . . . . . 9
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
21 | 19, 20 | exlimih 1573 |
. . . . . . . 8
⊢
(∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) |
22 | 21 | con3i 622 |
. . . . . . 7
⊢ (¬
∃𝑥𝜑 → ¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓)) |
23 | | mon 2035 |
. . . . . . 7
⊢ (¬
∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
24 | 22, 23 | syl 14 |
. . . . . 6
⊢ (¬
∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
25 | 24 | a1d 22 |
. . . . 5
⊢ (¬
∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
26 | 25 | a1d 22 |
. . . 4
⊢ (¬
∃𝑥𝜑 → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
27 | 18, 26 | jaoi 706 |
. . 3
⊢
((∃𝑥𝜑 ∨ ¬ ∃𝑥𝜑) → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
28 | 27 | impd 252 |
. 2
⊢
((∃𝑥𝜑 ∨ ¬ ∃𝑥𝜑) → ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
29 | 1, 28 | sylbi 120 |
1
⊢
(DECID ∃𝑥𝜑 → ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |