Theorem coundi 6278

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 5248	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))}
2		brun 5217	. . . . . . . 8 ⊢ (𝑥(𝐵 ∪ 𝐶)𝑧 ↔ (𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧))
3	2	anbi1i 623	. . . . . . 7 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4		andir 1009	. . . . . . 7 ⊢ (((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
5	3, 4	bitri 275	. . . . . 6 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
6	5	exbii 1846	. . . . 5 ⊢ (∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
7		19.43 1881	. . . . 5 ⊢ (∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
8	6, 7	bitr2i 276	. . . 4 ⊢ ((∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
9	8	opabbii 5233	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
10	1, 9	eqtri 2768	. 2 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
11		df-co 5709	. . 3 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
12		df-co 5709	. . 3 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}
13	11, 12	uneq12i 4189	. 2 ⊢ ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)})
14		df-co 5709	. 2 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
15	10, 13, 14	3eqtr4ri 2779	1 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

Syntax hints:   ∧ wa 395   ∨ wo 846   = wceq 1537  ∃wex 1777   ∪ cun 3974   class class class wbr 5166  {copab 5228   ∘ ccom 5704

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-br 5167  df-opab 5229  df-co 5709

This theorem is referenced by:  f1ofvswap  7342  mvdco  19487  ustssco  24244  coprprop  32711  cycpmconjv  33135  cvmliftlem10  35262  poimirlem9  37589  diophren  42769  rtrclex  43579  trclubgNEW  43580  trclexi  43582  rtrclexi  43583  cnvtrcl0  43588  trrelsuperrel2dg  43633  cotrclrcl  43704  frege131d  43726