Proof of Theorem mo3h
Step | Hyp | Ref
| Expression |
1 | | mo3h.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦𝜑) |
2 | 1 | nfi 1351 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
3 | 2 | eu2 1944 |
. . . . 5
⊢
(∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
4 | 3 | imbi2i 215 |
. . . 4
⊢
((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑥𝜑 → (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
5 | | df-mo 1904 |
. . . 4
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
6 | | anclb 302 |
. . . 4
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 → (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
7 | 4, 5, 6 | 3bitr4i 201 |
. . 3
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
8 | | 19.38 1566 |
. . . . 5
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥(𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
9 | 2 | 19.21 1475 |
. . . . . 6
⊢
(∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
10 | 9 | albii 1359 |
. . . . 5
⊢
(∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ ∀𝑥(𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
11 | 8, 10 | sylibr 137 |
. . . 4
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
12 | | anabs5 507 |
. . . . . 6
⊢ ((𝜑 ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) ↔ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) |
13 | | pm3.31 249 |
. . . . . 6
⊢ ((𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ((𝜑 ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) → 𝑥 = 𝑦)) |
14 | 12, 13 | syl5bir 142 |
. . . . 5
⊢ ((𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
15 | 14 | 2alimi 1345 |
. . . 4
⊢
(∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
16 | 11, 15 | syl 14 |
. . 3
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
17 | 7, 16 | sylbi 114 |
. 2
⊢
(∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
18 | 3 | simplbi2com 1333 |
. . 3
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃!𝑥𝜑)) |
19 | 18, 5 | sylibr 137 |
. 2
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑) |
20 | 17, 19 | impbii 117 |
1
⊢
(∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |