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

Metamath Proof Explorer

Theorem xpiundir

Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014)

Ref Expression
Assertion xpiundir 
|- ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )

Proof

Step Hyp Ref Expression
1 rexcom4 
 |-  ( E. x e. A E. y ( y e. B /\ E. w e. C z = <. y , w >. ) <-> E. y E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
2 df-rex 
 |-  ( E. y e. B E. w e. C z = <. y , w >. <-> E. y ( y e. B /\ E. w e. C z = <. y , w >. ) )
3 2 rexbii 
 |-  ( E. x e. A E. y e. B E. w e. C z = <. y , w >. <-> E. x e. A E. y ( y e. B /\ E. w e. C z = <. y , w >. ) )
4 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
5 4 anbi1i 
 |-  ( ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> ( E. x e. A y e. B /\ E. w e. C z = <. y , w >. ) )
6 r19.41v 
 |-  ( E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) <-> ( E. x e. A y e. B /\ E. w e. C z = <. y , w >. ) )
7 5 6 bitr4i 
 |-  ( ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
8 7 exbii 
 |-  ( E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. y E. x e. A ( y e. B /\ E. w e. C z = <. y , w >. ) )
9 1 3 8 3bitr4ri 
 |-  ( E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) <-> E. x e. A E. y e. B E. w e. C z = <. y , w >. )
10 df-rex 
 |-  ( E. y e. U_ x e. A B E. w e. C z = <. y , w >. <-> E. y ( y e. U_ x e. A B /\ E. w e. C z = <. y , w >. ) )
11 elxp2 
 |-  ( z e. ( B X. C ) <-> E. y e. B E. w e. C z = <. y , w >. )
12 11 rexbii 
 |-  ( E. x e. A z e. ( B X. C ) <-> E. x e. A E. y e. B E. w e. C z = <. y , w >. )
13 9 10 12 3bitr4i 
 |-  ( E. y e. U_ x e. A B E. w e. C z = <. y , w >. <-> E. x e. A z e. ( B X. C ) )
14 elxp2 
 |-  ( z e. ( U_ x e. A B X. C ) <-> E. y e. U_ x e. A B E. w e. C z = <. y , w >. )
15 eliun 
 |-  ( z e. U_ x e. A ( B X. C ) <-> E. x e. A z e. ( B X. C ) )
16 13 14 15 3bitr4i 
 |-  ( z e. ( U_ x e. A B X. C ) <-> z e. U_ x e. A ( B X. C ) )
17 16 eqriv 
 |-  ( U_ x e. A B X. C ) = U_ x e. A ( B X. C )