Theorem coundi 6094

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 5137	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))}
2		brun 5109	. . . . . . . 8 ⊢ (𝑥(𝐵 ∪ 𝐶)𝑧 ↔ (𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧))
3	2	anbi1i 625	. . . . . . 7 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦))
4		andir 1005	. . . . . . 7 ⊢ (((𝑥𝐵𝑧 ∨ 𝑥𝐶𝑧) ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
5	3, 4	bitri 277	. . . . . 6 ⊢ ((𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
6	5	exbii 1844	. . . . 5 ⊢ (∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
7		19.43 1879	. . . . 5 ⊢ (∃𝑧((𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ (𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)))
8	6, 7	bitr2i 278	. . . 4 ⊢ ((∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
9	8	opabbii 5125	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ∨ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
10	1, 9	eqtri 2844	. 2 ⊢ ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
11		df-co 5558	. . 3 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
12		df-co 5558	. . 3 ⊢ (𝐴 ∘ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)}
13	11, 12	uneq12i 4136	. 2 ⊢ ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) = ({⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐶𝑧 ∧ 𝑧𝐴𝑦)})
14		df-co 5558	. 2 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥(𝐵 ∪ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)}
15	10, 13, 14	3eqtr4ri 2855	1 ⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶))

Syntax hints:   ∧ wa 398   ∨ wo 843   = wceq 1533  ∃wex 1776   ∪ cun 3933   class class class wbr 5058  {copab 5120   ∘ ccom 5553

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-br 5059  df-opab 5121  df-co 5558

This theorem is referenced by:  mvdco  18567  ustssco  22817  coprprop  30429  cycpmconjv  30779  cvmliftlem10  32536  poimirlem9  34895  diophren  39403  rtrclex  39970  trclubgNEW  39971  trclexi  39973  rtrclexi  39974  cnvtrcl0  39979  trrelsuperrel2dg  40009  cotrclrcl  40080  frege131d  40102