Theorem coiun

Description: Composition with an indexed union. (Contributed by NM, 21-Dec-2008)

	Ref	Expression
Assertion	coiun	$$⊢A\circ \bigcup _{x\in C}B=\bigcup _{x\in C}\left(A\circ B\right)$$

Proof

Step	Hyp	Ref	Expression
1		relco	$$⊢\mathrm{Rel}\left(A\circ \bigcup _{x\in C}B\right)$$
2		reliun	$$⊢\mathrm{Rel}\bigcup _{x\in C}\left(A\circ B\right)\leftrightarrow \forall x\in C\mathrm{Rel}\left(A\circ B\right)$$
3		relco	$$⊢\mathrm{Rel}\left(A\circ B\right)$$
4	3	a1i	$$⊢x\in C\to \mathrm{Rel}\left(A\circ B\right)$$
5	2 4	mprgbir	$$⊢\mathrm{Rel}\bigcup _{x\in C}\left(A\circ B\right)$$
6		eliun	$$⊢⟨y,w⟩\in \bigcup _{x\in C}B\leftrightarrow \exists x\in C⟨y,w⟩\in B$$
7		df-br	$$⊢y\bigcup _{x\in C}Bw\leftrightarrow ⟨y,w⟩\in \bigcup _{x\in C}B$$
8		df-br	$$⊢yBw\leftrightarrow ⟨y,w⟩\in B$$
9	8	rexbii	$$⊢\exists x\in CyBw\leftrightarrow \exists x\in C⟨y,w⟩\in B$$
10	6 7 9	3bitr4i	$$⊢y\bigcup _{x\in C}Bw\leftrightarrow \exists x\in CyBw$$
11	10	anbi1i	$$⊢\left(y\bigcup _{x\in C}Bw\wedge wAz\right)\leftrightarrow \left(\exists x\in CyBw\wedge wAz\right)$$
12		r19.41v	$$⊢\exists x\in C\left(yBw\wedge wAz\right)\leftrightarrow \left(\exists x\in CyBw\wedge wAz\right)$$
13	11 12	bitr4i	$$⊢\left(y\bigcup _{x\in C}Bw\wedge wAz\right)\leftrightarrow \exists x\in C\left(yBw\wedge wAz\right)$$
14	13	exbii	$$⊢\exists w\left(y\bigcup _{x\in C}Bw\wedge wAz\right)\leftrightarrow \exists w\exists x\in C\left(yBw\wedge wAz\right)$$
15		rexcom4	$$⊢\exists x\in C\exists w\left(yBw\wedge wAz\right)\leftrightarrow \exists w\exists x\in C\left(yBw\wedge wAz\right)$$
16	14 15	bitr4i	$$⊢\exists w\left(y\bigcup _{x\in C}Bw\wedge wAz\right)\leftrightarrow \exists x\in C\exists w\left(yBw\wedge wAz\right)$$
17		vex	$$⊢y\in \mathrm{V}$$
18		vex	$$⊢z\in \mathrm{V}$$
19	17 18	opelco	$$⊢⟨y,z⟩\in \left(A\circ \bigcup _{x\in C}B\right)\leftrightarrow \exists w\left(y\bigcup _{x\in C}Bw\wedge wAz\right)$$
20	17 18	opelco	$$⊢⟨y,z⟩\in \left(A\circ B\right)\leftrightarrow \exists w\left(yBw\wedge wAz\right)$$
21	20	rexbii	$$⊢\exists x\in C⟨y,z⟩\in \left(A\circ B\right)\leftrightarrow \exists x\in C\exists w\left(yBw\wedge wAz\right)$$
22	16 19 21	3bitr4i	$$⊢⟨y,z⟩\in \left(A\circ \bigcup _{x\in C}B\right)\leftrightarrow \exists x\in C⟨y,z⟩\in \left(A\circ B\right)$$
23		eliun	$$⊢⟨y,z⟩\in \bigcup _{x\in C}\left(A\circ B\right)\leftrightarrow \exists x\in C⟨y,z⟩\in \left(A\circ B\right)$$
24	22 23	bitr4i	$$⊢⟨y,z⟩\in \left(A\circ \bigcup _{x\in C}B\right)\leftrightarrow ⟨y,z⟩\in \bigcup _{x\in C}\left(A\circ B\right)$$
25	1 5 24	eqrelriiv	$$⊢A\circ \bigcup _{x\in C}B=\bigcup _{x\in C}\left(A\circ B\right)$$