Proof of Theorem mo3h
Step | Hyp | Ref
| Expression |
1 | | mo3h.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦𝜑) |
2 | 1 | nfi 1462 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
3 | 2 | eu2 2070 |
. . . . 5
⊢
(∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
4 | 3 | imbi2i 226 |
. . . 4
⊢
((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑥𝜑 → (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
5 | | df-mo 2030 |
. . . 4
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) |
6 | | anclb 319 |
. . . 4
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 → (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))) |
7 | 4, 5, 6 | 3bitr4i 212 |
. . 3
⊢
(∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
8 | | 19.38 1676 |
. . . . 5
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥(𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
9 | 2 | 19.21 1583 |
. . . . . 6
⊢
(∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
10 | 9 | albii 1470 |
. . . . 5
⊢
(∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ ∀𝑥(𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
11 | 8, 10 | sylibr 134 |
. . . 4
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) |
12 | | anabs5 573 |
. . . . . 6
⊢ ((𝜑 ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) ↔ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) |
13 | | pm3.31 262 |
. . . . . 6
⊢ ((𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ((𝜑 ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) → 𝑥 = 𝑦)) |
14 | 12, 13 | biimtrrid 153 |
. . . . 5
⊢ ((𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
15 | 14 | 2alimi 1456 |
. . . 4
⊢
(∀𝑥∀𝑦(𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
16 | 11, 15 | syl 14 |
. . 3
⊢
((∃𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
17 | 7, 16 | sylbi 121 |
. 2
⊢
(∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |
18 | 3 | simplbi2com 1444 |
. . 3
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃!𝑥𝜑)) |
19 | 18, 5 | sylibr 134 |
. 2
⊢
(∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑) |
20 | 17, 19 | impbii 126 |
1
⊢
(∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) |