Theorem xpundir 5721

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.

Step	Hyp	Ref	Expression
1		df-xp 5657	. 2 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)}
2		df-xp 5657	. . . 4 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
3		df-xp 5657	. . . 4 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
4	2, 3	uneq12i 4113	. . 3 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
5		elun 4100	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
6	5	anbi1i 636	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶))
7		andir 1026	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
8	6, 7	bitri 278	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
9	8	opabbii 5172	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
10		unopab 5185	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
11	9, 10	eqtr4i 2787	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
12	4, 11	eqtr4i 2787	. 2 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)}
13	1, 12	eqtr4i 2787	1 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ cun 3897  {copab 5167   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-opab 5168  df-xp 5657

This theorem is used by:  xpun  5725  resundi  5984  xpprsng  7142  naddasslem1  8704  xp2dju  10255  alephadd  10662  hashxplem  14578  ustund  24541  cnmpopc  25249  poimirlem3  38541  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem16  38554  poimirlem19  38557  fsuppssind  43621  pwssplit4  44090