Proof of Theorem mo2v
Step | Hyp | Ref
| Expression |
1 | | df-mo 2463 |
. 2
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
2 | | df-eu 2462 |
. . 3
⊢
(∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
3 | 2 | imbi2i 325 |
. 2
⊢
((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
4 | | alnex 1697 |
. . . . . . 7
⊢
(∀𝑥 ¬
𝜑 ↔ ¬ ∃𝑥𝜑) |
5 | | pm2.21 119 |
. . . . . . . 8
⊢ (¬
𝜑 → (𝜑 → 𝑥 = 𝑦)) |
6 | 5 | alimi 1730 |
. . . . . . 7
⊢
(∀𝑥 ¬
𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
7 | 4, 6 | sylbir 224 |
. . . . . 6
⊢ (¬
∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
8 | 7 | eximi 1752 |
. . . . 5
⊢
(∃𝑦 ¬
∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
9 | 8 | 19.23bi 2049 |
. . . 4
⊢ (¬
∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
10 | | biimp 204 |
. . . . . 6
⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦)) |
11 | 10 | alimi 1730 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
12 | 11 | eximi 1752 |
. . . 4
⊢
(∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
13 | 9, 12 | ja 172 |
. . 3
⊢
((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
14 | | nfia1 2017 |
. . . . . 6
⊢
Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
15 | | id 22 |
. . . . . . . . . 10
⊢ (𝜑 → 𝜑) |
16 | | ax12v 2035 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
17 | 16 | com12 32 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
18 | 15, 17 | embantd 57 |
. . . . . . . . 9
⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
19 | 18 | spsd 2045 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
20 | 19 | ancld 574 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
21 | | albiim 1806 |
. . . . . . 7
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
22 | 20, 21 | syl6ibr 241 |
. . . . . 6
⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
23 | 14, 22 | exlimi 2073 |
. . . . 5
⊢
(∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
24 | 23 | eximdv 1833 |
. . . 4
⊢
(∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
25 | 24 | com12 32 |
. . 3
⊢
(∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) |
26 | 13, 25 | impbii 198 |
. 2
⊢
((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
27 | 1, 3, 26 | 3bitri 285 |
1
⊢
(∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |