![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xpundir | Structured version Visualization version GIF version |
Description: Distributive law for Cartesian product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.) |
Ref | Expression |
---|---|
xpundir | ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xp 5525 | . 2 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} | |
2 | df-xp 5525 | . . . 4 ⊢ (𝐴 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} | |
3 | df-xp 5525 | . . . 4 ⊢ (𝐵 × 𝐶) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} | |
4 | 2, 3 | uneq12i 4088 | . . 3 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
5 | elun 4076 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
6 | 5 | anbi1i 626 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶)) |
7 | andir 1006 | . . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) | |
8 | 6, 7 | bitri 278 | . . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
9 | 8 | opabbii 5097 | . . . 4 ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} |
10 | unopab 5109 | . . . 4 ⊢ ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} | |
11 | 9, 10 | eqtr4i 2824 | . . 3 ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) |
12 | 4, 11 | eqtr4i 2824 | . 2 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} |
13 | 1, 12 | eqtr4i 2824 | 1 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 ∨ wo 844 = wceq 1538 ∈ wcel 2111 ∪ cun 3879 {copab 5092 × cxp 5517 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-opab 5093 df-xp 5525 |
This theorem is referenced by: xpun 5589 resundi 5832 xpprsng 6879 xpfi 8773 xp2dju 9587 alephadd 9988 hashxplem 13790 ustund 22827 cnmpopc 23533 poimirlem3 35060 poimirlem4 35061 poimirlem6 35063 poimirlem7 35064 poimirlem16 35073 poimirlem19 35076 fsuppssind 39459 pwssplit4 40033 |
Copyright terms: Public domain | W3C validator |