Theorem coiun

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

	Ref	Expression
Assertion	coiun	|- ( A o. U_ x e. C B ) = U_ x e. C ( A o. B )

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( A o. U_ x e. C B )
2		reliun	|- ( Rel U_ x e. C ( A o. B ) <-> A. x e. C Rel ( A o. B ) )
3		relco	|- Rel ( A o. B )
4	3	a1i	|- ( x e. C -> Rel ( A o. B ) )
5	2 4	mprgbir	|- Rel U_ x e. C ( A o. B )
6		eliun	|- ( <. y , w >. e. U_ x e. C B <-> E. x e. C <. y , w >. e. B )
7		df-br	|- ( y U_ x e. C B w <-> <. y , w >. e. U_ x e. C B )
8		df-br	|- ( y B w <-> <. y , w >. e. B )
9	8	rexbii	|- ( E. x e. C y B w <-> E. x e. C <. y , w >. e. B )
10	6 7 9	3bitr4i	|- ( y U_ x e. C B w <-> E. x e. C y B w )
11	10	anbi1i	|- ( ( y U_ x e. C B w /\ w A z ) <-> ( E. x e. C y B w /\ w A z ) )
12		r19.41v	|- ( E. x e. C ( y B w /\ w A z ) <-> ( E. x e. C y B w /\ w A z ) )
13	11 12	bitr4i	|- ( ( y U_ x e. C B w /\ w A z ) <-> E. x e. C ( y B w /\ w A z ) )
14	13	exbii	|- ( E. w ( y U_ x e. C B w /\ w A z ) <-> E. w E. x e. C ( y B w /\ w A z ) )
15		rexcom4	|- ( E. x e. C E. w ( y B w /\ w A z ) <-> E. w E. x e. C ( y B w /\ w A z ) )
16	14 15	bitr4i	|- ( E. w ( y U_ x e. C B w /\ w A z ) <-> E. x e. C E. w ( y B w /\ w A z ) )
17		vex	|- y e. _V
18		vex	|- z e. _V
19	17 18	opelco	|- ( <. y , z >. e. ( A o. U_ x e. C B ) <-> E. w ( y U_ x e. C B w /\ w A z ) )
20	17 18	opelco	|- ( <. y , z >. e. ( A o. B ) <-> E. w ( y B w /\ w A z ) )
21	20	rexbii	|- ( E. x e. C <. y , z >. e. ( A o. B ) <-> E. x e. C E. w ( y B w /\ w A z ) )
22	16 19 21	3bitr4i	|- ( <. y , z >. e. ( A o. U_ x e. C B ) <-> E. x e. C <. y , z >. e. ( A o. B ) )
23		eliun	|- ( <. y , z >. e. U_ x e. C ( A o. B ) <-> E. x e. C <. y , z >. e. ( A o. B ) )
24	22 23	bitr4i	|- ( <. y , z >. e. ( A o. U_ x e. C B ) <-> <. y , z >. e. U_ x e. C ( A o. B ) )
25	1 5 24	eqrelriiv	|- ( A o. U_ x e. C B ) = U_ x e. C ( A o. B )