Theorem xpundir 5769

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 5706	. 2 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)}
2		df-xp 5706	. . . 4 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
3		df-xp 5706	. . . 4 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
4	2, 3	uneq12i 4189	. . 3 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
5		elun 4176	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
6	5	anbi1i 623	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶))
7		andir 1009	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
8	6, 7	bitri 275	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
9	8	opabbii 5233	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
10		unopab 5248	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
11	9, 10	eqtr4i 2771	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)} = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
12	4, 11	eqtr4i 2771	. 2 ⊢ ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑦 ∈ 𝐶)}
13	1, 12	eqtr4i 2771	1 ⊢ ((𝐴 ∪ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∪ (𝐵 × 𝐶))

Syntax hints:   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ∪ cun 3974  {copab 5228   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-opab 5229  df-xp 5706

This theorem is referenced by:  xpun  5773  resundi  6023  xpprsng  7174  naddasslem1  8750  xpfiOLD  9387  xp2dju  10246  alephadd  10646  hashxplem  14482  ustund  24251  cnmpopc  24974  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem16  37596  poimirlem19  37599  fsuppssind  42548  pwssplit4  43046