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

Metamath Proof Explorer

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 ) )