Proof of Theorem euexex
Step | Hyp | Ref
| Expression |
1 | | eu5 2073 |
. . 3
⊢
(∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
2 | | nfmo1 2038 |
. . . . . 6
⊢
Ⅎ𝑥∃*𝑥𝜑 |
3 | | nfa1 1541 |
. . . . . . 7
⊢
Ⅎ𝑥∀𝑥∃*𝑦𝜓 |
4 | | nfe1 1496 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥(𝜑 ∧ 𝜓) |
5 | 4 | nfmo 2046 |
. . . . . . 7
⊢
Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓) |
6 | 3, 5 | nfim 1572 |
. . . . . 6
⊢
Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |
7 | 2, 6 | nfim 1572 |
. . . . 5
⊢
Ⅎ𝑥(∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
8 | | euexex.1 |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
9 | 8 | nfmo 2046 |
. . . . . . 7
⊢
Ⅎ𝑦∃*𝑥𝜑 |
10 | | mopick 2104 |
. . . . . . . . 9
⊢
((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) |
11 | 10 | ex 115 |
. . . . . . . 8
⊢
(∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓))) |
12 | 11 | com3r 79 |
. . . . . . 7
⊢ (𝜑 → (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
13 | 8, 9, 12 | alrimd 1610 |
. . . . . 6
⊢ (𝜑 → (∃*𝑥𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓))) |
14 | | moim 2090 |
. . . . . . 7
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
15 | 14 | spsd 1538 |
. . . . . 6
⊢
(∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
16 | 13, 15 | syl6 33 |
. . . . 5
⊢ (𝜑 → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
17 | 7, 16 | exlimi 1594 |
. . . 4
⊢
(∃𝑥𝜑 → (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))) |
18 | 17 | imp 124 |
. . 3
⊢
((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
19 | 1, 18 | sylbi 121 |
. 2
⊢
(∃!𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))) |
20 | 19 | imp 124 |
1
⊢
((∃!𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)) |