This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐶 ∪ 𝐷 ) ) = ( ( ( 𝐴 × 𝐶 ) ∪ ( 𝐴 × 𝐷 ) ) ∪ ( ( 𝐵 × 𝐶 ) ∪ ( 𝐵 × 𝐷 ) ) )