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 )

Metamath Proof Explorer

Theorem coiun

Proof