Theorem coundi 5553

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
coundi	⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

Proof of Theorem coundi

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unopab 4660	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))}
2		brun 4633	. . . . . . . 8 ⊢ (𝑥(𝐵 ∪ 𝐶)𝑧 ↔ (𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧))
3	2	anbi1i 727	. . . . . . 7 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4		andir 908	. . . . . . 7 ⊢ (((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
5	3, 4	bitri 263	. . . . . 6 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
6	5	exbii 1764	. . . . 5 ⊢ (∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
7		19.43 1799	. . . . 5 ⊢ (∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
8	6, 7	bitr2i 264	. . . 4 ⊢ ((∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
9	8	opabbii 4649	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
10	1, 9	eqtri 2632	. 2 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
11		df-co 5047	. . 3 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
12		df-co 5047	. . 3 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}
13	11, 12	uneq12i 3727	. 2 ⊢ ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)})
14		df-co 5047	. 2 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
15	10, 13, 14	3eqtr4ri 2643	1 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

Syntax hints:   ∨ wo 382   ∧ wa 383   = wceq 1475  ∃wex 1695   ∪ cun 3538   class class class wbr 4583  {copab 4642   ∘ ccom 5042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-br 4584  df-opab 4644  df-co 5047

This theorem is referenced by:  mvdco  17688  ustssco  21828  cvmliftlem10  30530  poimirlem9  32588  diophren  36395  rtrclex  36943  trclubgNEW  36944  trclexi  36946  rtrclexi  36947  cnvtrcl0  36952  trrelsuperrel2dg  36982  cotrclrcl  37053  frege131d  37075