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

Theorem xpundir 5745
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 5682 . 2 ((𝐴𝐵) × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
2 df-xp 5682 . . . 4 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
3 df-xp 5682 . . . 4 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
42, 3uneq12i 4161 . . 3 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
5 elun 4148 . . . . . . 7 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 624 . . . . . 6 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶))
7 andir 1007 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
86, 7bitri 274 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
98opabbii 5215 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
10 unopab 5230 . . . 4 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
119, 10eqtr4i 2763 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
124, 11eqtr4i 2763 . 2 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
131, 12eqtr4i 2763 1 ((𝐴𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 396  wo 845   = wceq 1541  wcel 2106  cun 3946  {copab 5210   × cxp 5674
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-opab 5211  df-xp 5682
This theorem is referenced by:  xpun  5749  resundi  5995  xpprsng  7140  naddasslem1  8695  xpfiOLD  9320  xp2dju  10173  alephadd  10574  hashxplem  14395  ustund  23733  cnmpopc  24451  poimirlem3  36577  poimirlem4  36578  poimirlem6  36580  poimirlem7  36581  poimirlem16  36590  poimirlem19  36593  fsuppssind  41247  pwssplit4  41913
  Copyright terms: Public domain W3C validator