Proof of Theorem fnoprabg
| Step | Hyp | Ref
| Expression |
| 1 | | eumo 2578 |
. . . . . 6
⊢
(∃!𝑧𝜓 → ∃*𝑧𝜓) |
| 2 | 1 | imim2i 16 |
. . . . 5
⊢ ((𝜑 → ∃!𝑧𝜓) → (𝜑 → ∃*𝑧𝜓)) |
| 3 | | moanimv 2619 |
. . . . 5
⊢
(∃*𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑧𝜓)) |
| 4 | 2, 3 | sylibr 234 |
. . . 4
⊢ ((𝜑 → ∃!𝑧𝜓) → ∃*𝑧(𝜑 ∧ 𝜓)) |
| 5 | 4 | 2alimi 1812 |
. . 3
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → ∀𝑥∀𝑦∃*𝑧(𝜑 ∧ 𝜓)) |
| 6 | | funoprabg 7554 |
. . 3
⊢
(∀𝑥∀𝑦∃*𝑧(𝜑 ∧ 𝜓) → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)}) |
| 7 | 5, 6 | syl 17 |
. 2
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)}) |
| 8 | | dmoprab 7536 |
. . 3
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝜑 ∧ 𝜓)} |
| 9 | | nfa1 2151 |
. . . 4
⊢
Ⅎ𝑥∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) |
| 10 | | nfa2 2176 |
. . . 4
⊢
Ⅎ𝑦∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) |
| 11 | | simpl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
| 12 | 11 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑧(𝜑 ∧ 𝜓) → 𝜑) |
| 13 | | euex 2577 |
. . . . . . . . . 10
⊢
(∃!𝑧𝜓 → ∃𝑧𝜓) |
| 14 | 13 | imim2i 16 |
. . . . . . . . 9
⊢ ((𝜑 → ∃!𝑧𝜓) → (𝜑 → ∃𝑧𝜓)) |
| 15 | 14 | ancld 550 |
. . . . . . . 8
⊢ ((𝜑 → ∃!𝑧𝜓) → (𝜑 → (𝜑 ∧ ∃𝑧𝜓))) |
| 16 | | 19.42v 1953 |
. . . . . . . 8
⊢
(∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑧𝜓)) |
| 17 | 15, 16 | imbitrrdi 252 |
. . . . . . 7
⊢ ((𝜑 → ∃!𝑧𝜓) → (𝜑 → ∃𝑧(𝜑 ∧ 𝜓))) |
| 18 | 12, 17 | impbid2 226 |
. . . . . 6
⊢ ((𝜑 → ∃!𝑧𝜓) → (∃𝑧(𝜑 ∧ 𝜓) ↔ 𝜑)) |
| 19 | 18 | sps 2185 |
. . . . 5
⊢
(∀𝑦(𝜑 → ∃!𝑧𝜓) → (∃𝑧(𝜑 ∧ 𝜓) ↔ 𝜑)) |
| 20 | 19 | sps 2185 |
. . . 4
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → (∃𝑧(𝜑 ∧ 𝜓) ↔ 𝜑)) |
| 21 | 9, 10, 20 | opabbid 5208 |
. . 3
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝜑 ∧ 𝜓)} = {〈𝑥, 𝑦〉 ∣ 𝜑}) |
| 22 | 8, 21 | eqtrid 2789 |
. 2
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} = {〈𝑥, 𝑦〉 ∣ 𝜑}) |
| 23 | | df-fn 6564 |
. 2
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ (Fun {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} ∧ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} = {〈𝑥, 𝑦〉 ∣ 𝜑})) |
| 24 | 7, 22, 23 | sylanbrc 583 |
1
⊢
(∀𝑥∀𝑦(𝜑 → ∃!𝑧𝜓) → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ (𝜑 ∧ 𝜓)} Fn {〈𝑥, 𝑦〉 ∣ 𝜑}) |