MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpundir Structured version   Visualization version   GIF version

Theorem xpundir 5594
Description: Distributive law for Cartesian product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
Assertion
Ref Expression
xpundir ((𝐴𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))

Proof of Theorem xpundir
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-xp 5534 . 2 ((𝐴𝐵) × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
2 df-xp 5534 . . . 4 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
3 df-xp 5534 . . . 4 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
42, 3uneq12i 4113 . . 3 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
5 elun 4101 . . . . . . 7 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 626 . . . . . 6 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶))
7 andir 1006 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
86, 7bitri 278 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
98opabbii 5106 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
10 unopab 5118 . . . 4 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
119, 10eqtr4i 2847 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
124, 11eqtr4i 2847 . 2 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
131, 12eqtr4i 2847 1 ((𝐴𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 399  wo 844   = wceq 1538  wcel 2115  cun 3908  {copab 5101   × cxp 5526
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-un 3915  df-opab 5102  df-xp 5534
This theorem is referenced by:  xpun  5598  resundi  5840  xpprsng  6875  xpfi  8765  xp2dju  9579  alephadd  9976  hashxplem  13778  ustund  22805  cnmpopc  23511  poimirlem3  34938  poimirlem4  34939  poimirlem6  34941  poimirlem7  34942  poimirlem16  34951  poimirlem19  34954  pwssplit4  39828
  Copyright terms: Public domain W3C validator