| Step | Hyp | Ref
| Expression |
| 1 | | df-mpo 7436 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} |
| 2 | | df-oprab 7435 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)} = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} |
| 3 | 1, 2 | eqtri 2765 |
. 2
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} |
| 4 | | nel02 4339 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴) |
| 5 | | nel02 4339 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵) |
| 6 | 4, 5 | orim12i 909 |
. . . . . . . . 9
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵)) |
| 7 | | ianor 984 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵)) |
| 8 | 6, 7 | sylibr 234 |
. . . . . . . 8
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 9 | | simprl 771 |
. . . . . . . 8
⊢ ((𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 10 | 8, 9 | nsyl 140 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 11 | 10 | nexdv 1936 |
. . . . . 6
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬
∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 12 | 11 | nexdv 1936 |
. . . . 5
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬
∃𝑦∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 13 | 12 | nexdv 1936 |
. . . 4
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ¬
∃𝑥∃𝑦∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 14 | 13 | alrimiv 1927 |
. . 3
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 15 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ↔ 𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉)) |
| 16 | 15 | anbi1d 631 |
. . . . 5
⊢ (𝑧 = 𝑣 → ((𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ (𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))) |
| 17 | 16 | 3exbidv 1925 |
. . . 4
⊢ (𝑧 = 𝑣 → (∃𝑥∃𝑦∃𝑤(𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)) ↔ ∃𝑥∃𝑦∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶)))) |
| 18 | 17 | ab0w 4379 |
. . 3
⊢ ({𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅ ↔ ∀𝑣 ¬ ∃𝑥∃𝑦∃𝑤(𝑣 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))) |
| 19 | 14, 18 | sylibr 234 |
. 2
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → {𝑧 ∣ ∃𝑥∃𝑦∃𝑤(𝑧 = 〈〈𝑥, 𝑦〉, 𝑤〉 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑤 = 𝐶))} = ∅) |
| 20 | 3, 19 | eqtrid 2789 |
1
⊢ ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = ∅) |