Theorem xpundi

Description: Distributive law for Cartesian product over union. Theorem 103 of Suppes p. 52. (Contributed by NM, 12-Aug-2004)

	Ref	Expression
Assertion	xpundi	|- ( A X. ( B u. C ) ) = ( ( A X. B ) u. ( A X. C ) )

Proof

Step	Hyp	Ref	Expression
1		df-xp	|- ( A X. ( B u. C ) ) = { <. x , y >. | ( x e. A /\ y e. ( B u. C ) ) }
2		df-xp	|- ( A X. B ) = { <. x , y >. | ( x e. A /\ y e. B ) }
3		df-xp	|- ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
4	2 3	uneq12i	|- ( ( A X. B ) u. ( A X. C ) ) = ( { <. x , y >. | ( x e. A /\ y e. B ) } u. { <. x , y >. | ( x e. A /\ y e. C ) } )
5		elun	|- ( y e. ( B u. C ) <-> ( y e. B \/ y e. C ) )
6	5	anbi2i	|- ( ( x e. A /\ y e. ( B u. C ) ) <-> ( x e. A /\ ( y e. B \/ y e. C ) ) )
7		andi	|- ( ( x e. A /\ ( y e. B \/ y e. C ) ) <-> ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) )
8	6 7	bitri	|- ( ( x e. A /\ y e. ( B u. C ) ) <-> ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) )
9	8	opabbii	|- { <. x , y >. | ( x e. A /\ y e. ( B u. C ) ) } = { <. x , y >. | ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) }
10		unopab	|- ( { <. x , y >. | ( x e. A /\ y e. B ) } u. { <. x , y >. | ( x e. A /\ y e. C ) } ) = { <. x , y >. | ( ( x e. A /\ y e. B ) \/ ( x e. A /\ y e. C ) ) }
11	9 10	eqtr4i	|- { <. x , y >. | ( x e. A /\ y e. ( B u. C ) ) } = ( { <. x , y >. | ( x e. A /\ y e. B ) } u. { <. x , y >. | ( x e. A /\ y e. C ) } )
12	4 11	eqtr4i	|- ( ( A X. B ) u. ( A X. C ) ) = { <. x , y >. | ( x e. A /\ y e. ( B u. C ) ) }
13	1 12	eqtr4i	|- ( A X. ( B u. C ) ) = ( ( A X. B ) u. ( A X. C ) )