Step | Hyp | Ref
| Expression |
1 | | unopab 4043 |
. . 3
⊢
({〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {〈𝑥, 𝑦〉 ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} |
2 | | brun 4015 |
. . . . . . . 8
⊢ (𝑥(𝐵 ∪ 𝐶)𝑧 ↔ (𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧)) |
3 | 2 | anbi1i 454 |
. . . . . . 7
⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦)) |
4 | | andir 809 |
. . . . . . 7
⊢ (((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))) |
5 | 3, 4 | bitri 183 |
. . . . . 6
⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))) |
6 | 5 | exbii 1585 |
. . . . 5
⊢
(∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))) |
7 | | 19.43 1608 |
. . . . 5
⊢
(∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))) |
8 | 6, 7 | bitr2i 184 |
. . . 4
⊢
((∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)) |
9 | 8 | opabbii 4031 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)} |
10 | 1, 9 | eqtri 2178 |
. 2
⊢
({〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)} |
11 | | df-co 4595 |
. . 3
⊢ (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} |
12 | | df-co 4595 |
. . 3
⊢ (𝐴 ∘ 𝐶) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)} |
13 | 11, 12 | uneq12i 3259 |
. 2
⊢ ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) = ({〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) |
14 | | df-co 4595 |
. 2
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)} |
15 | 10, 13, 14 | 3eqtr4ri 2189 |
1
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) |