Proof of Theorem euexex
Step | Hyp | Ref
| Expression |
1 | | eu5 1944 |
. . 3
⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ)) |
2 | | nfmo1 1909 |
. . . . . 6
⊢
Ⅎx∃*xφ |
3 | | nfa1 1431 |
. . . . . . 7
⊢
Ⅎx∀x∃*yψ |
4 | | nfe1 1382 |
. . . . . . . 8
⊢
Ⅎx∃x(φ ∧ ψ) |
5 | 4 | nfmo 1917 |
. . . . . . 7
⊢
Ⅎx∃*y∃x(φ ∧ ψ) |
6 | 3, 5 | nfim 1461 |
. . . . . 6
⊢
Ⅎx(∀x∃*yψ → ∃*y∃x(φ ∧ ψ)) |
7 | 2, 6 | nfim 1461 |
. . . . 5
⊢
Ⅎx(∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))) |
8 | | euexex.1 |
. . . . . . 7
⊢
Ⅎyφ |
9 | 8 | nfmo 1917 |
. . . . . . 7
⊢
Ⅎy∃*xφ |
10 | | mopick 1975 |
. . . . . . . . 9
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ)) |
11 | 10 | ex 108 |
. . . . . . . 8
⊢ (∃*xφ → (∃x(φ ∧ ψ) → (φ → ψ))) |
12 | 11 | com3r 73 |
. . . . . . 7
⊢ (φ → (∃*xφ → (∃x(φ ∧ ψ) → ψ))) |
13 | 8, 9, 12 | alrimd 1498 |
. . . . . 6
⊢ (φ → (∃*xφ → ∀y(∃x(φ ∧ ψ) → ψ))) |
14 | | moim 1961 |
. . . . . . 7
⊢ (∀y(∃x(φ ∧ ψ) → ψ) → (∃*yψ → ∃*y∃x(φ ∧ ψ))) |
15 | 14 | spsd 1428 |
. . . . . 6
⊢ (∀y(∃x(φ ∧ ψ) → ψ) → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))) |
16 | 13, 15 | syl6 29 |
. . . . 5
⊢ (φ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))) |
17 | 7, 16 | exlimi 1482 |
. . . 4
⊢ (∃xφ → (∃*xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ)))) |
18 | 17 | imp 115 |
. . 3
⊢ ((∃xφ ∧ ∃*xφ) → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))) |
19 | 1, 18 | sylbi 114 |
. 2
⊢ (∃!xφ → (∀x∃*yψ → ∃*y∃x(φ ∧ ψ))) |
20 | 19 | imp 115 |
1
⊢ ((∃!xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ)) |