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 
|- ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )

Proof

Step Hyp Ref Expression
1 xpundi 
 |-  ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A u. B ) X. C ) u. ( ( A u. B ) X. D ) )
2 xpundir 
 |-  ( ( A u. B ) X. C ) = ( ( A X. C ) u. ( B X. C ) )
3 xpundir 
 |-  ( ( A u. B ) X. D ) = ( ( A X. D ) u. ( B X. D ) )
4 2 3 uneq12i 
 |-  ( ( ( A u. B ) X. C ) u. ( ( A u. B ) X. D ) ) = ( ( ( A X. C ) u. ( B X. C ) ) u. ( ( A X. D ) u. ( B X. D ) ) )
5 un4 
 |-  ( ( ( A X. C ) u. ( B X. C ) ) u. ( ( A X. D ) u. ( B X. D ) ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )
6 1 4 5 3eqtri 
 |-  ( ( A u. B ) X. ( C u. D ) ) = ( ( ( A X. C ) u. ( A X. D ) ) u. ( ( B X. C ) u. ( B X. D ) ) )