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

Theorem xpundir 5758
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 5695 . 2 ((𝐴𝐵) × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
2 df-xp 5695 . . . 4 (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)}
3 df-xp 5695 . . . 4 (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}
42, 3uneq12i 4176 . . 3 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
5 elun 4163 . . . . . . 7 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
65anbi1i 624 . . . . . 6 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶))
7 andir 1010 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
86, 7bitri 275 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶) ↔ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶)))
98opabbii 5215 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
10 unopab 5230 . . . 4 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐶) ∨ (𝑥𝐵𝑦𝐶))}
119, 10eqtr4i 2766 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)} = ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐵𝑦𝐶)})
124, 11eqtr4i 2766 . 2 ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴𝐵) ∧ 𝑦𝐶)}
131, 12eqtr4i 2766 1 ((𝐴𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395  wo 847   = wceq 1537  wcel 2106  cun 3961  {copab 5210   × cxp 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-opab 5211  df-xp 5695
This theorem is referenced by:  xpun  5762  resundi  6014  xpprsng  7160  naddasslem1  8731  xpfiOLD  9357  xp2dju  10215  alephadd  10615  hashxplem  14469  ustund  24246  cnmpopc  24969  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem16  37623  poimirlem19  37626  fsuppssind  42580  pwssplit4  43078
  Copyright terms: Public domain W3C validator