Theorem xpundir

Description: Distributive law for Cartesian product over union. Similar to Theorem 103 of Suppes p. 52. (Contributed by NM, 30-Sep-2002)

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

Proof

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