Theorem xpun

Description: The Cartesian product of two unions. (Contributed by NM, 12-Aug-2004)

	Ref	Expression
Assertion	xpun	⊢ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐶 ∪ 𝐷 ) ) = ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐴 × 𝐷 ) ) ∪ ( ( 𝐵 × 𝐶 ) ∪ ( 𝐵 × 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpundi	⊢ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐶 ∪ 𝐷 ) ) = ( ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) ∪ ( ( 𝐴 ∪ 𝐵 ) × 𝐷 ) )
2		xpundir	⊢ ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) )
3		xpundir	⊢ ( ( 𝐴 ∪ 𝐵 ) × 𝐷 ) = ( ( 𝐴 × 𝐷 ) ∪ ( 𝐵 × 𝐷 ) )
4	2 3	uneq12i	⊢ ( ( ( 𝐴 ∪ 𝐵 ) × 𝐶 ) ∪ ( ( 𝐴 ∪ 𝐵 ) × 𝐷 ) ) = ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) ) ∪ ( ( 𝐴 × 𝐷 ) ∪ ( 𝐵 × 𝐷 ) ) )
5		un4	⊢ ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐵 × 𝐶 ) ) ∪ ( ( 𝐴 × 𝐷 ) ∪ ( 𝐵 × 𝐷 ) ) ) = ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐴 × 𝐷 ) ) ∪ ( ( 𝐵 × 𝐶 ) ∪ ( 𝐵 × 𝐷 ) ) )
6	1 4 5	3eqtri	⊢ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐶 ∪ 𝐷 ) ) = ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐴 × 𝐷 ) ) ∪ ( ( 𝐵 × 𝐶 ) ∪ ( 𝐵 × 𝐷 ) ) )