Metamath Proof Explorer

Theorem xpiindi

Description: Distributive law for Cartesian product over indexed intersection. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion xpiindi 
|- ( A =/= (/) -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( C X. B )
2 1 rgenw 
 |-  A. x e. A Rel ( C X. B )
3 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A Rel ( C X. B ) ) -> E. x e. A Rel ( C X. B ) )
4 2 3 mpan2 
 |-  ( A =/= (/) -> E. x e. A Rel ( C X. B ) )
5 reliin 
 |-  ( E. x e. A Rel ( C X. B ) -> Rel |^|_ x e. A ( C X. B ) )
6 4 5 syl 
 |-  ( A =/= (/) -> Rel |^|_ x e. A ( C X. B ) )
7 relxp 
 |-  Rel ( C X. |^|_ x e. A B )
8 6 7 jctil 
 |-  ( A =/= (/) -> ( Rel ( C X. |^|_ x e. A B ) /\ Rel |^|_ x e. A ( C X. B ) ) )
9 r19.28zv 
 |-  ( A =/= (/) -> ( A. x e. A ( y e. C /\ z e. B ) <-> ( y e. C /\ A. x e. A z e. B ) ) )
10 9 bicomd 
 |-  ( A =/= (/) -> ( ( y e. C /\ A. x e. A z e. B ) <-> A. x e. A ( y e. C /\ z e. B ) ) )
11 eliin 
 |-  ( z e. _V -> ( z e. |^|_ x e. A B <-> A. x e. A z e. B ) )
12 11 elv 
 |-  ( z e. |^|_ x e. A B <-> A. x e. A z e. B )
13 12 anbi2i 
 |-  ( ( y e. C /\ z e. |^|_ x e. A B ) <-> ( y e. C /\ A. x e. A z e. B ) )
14 opelxp 
 |-  ( <. y , z >. e. ( C X. B ) <-> ( y e. C /\ z e. B ) )
15 14 ralbii 
 |-  ( A. x e. A <. y , z >. e. ( C X. B ) <-> A. x e. A ( y e. C /\ z e. B ) )
16 10 13 15 3bitr4g 
 |-  ( A =/= (/) -> ( ( y e. C /\ z e. |^|_ x e. A B ) <-> A. x e. A <. y , z >. e. ( C X. B ) ) )
17 opelxp 
 |-  ( <. y , z >. e. ( C X. |^|_ x e. A B ) <-> ( y e. C /\ z e. |^|_ x e. A B ) )
18 opex 
 |-  <. y , z >. e. _V
19 eliin 
 |-  ( <. y , z >. e. _V -> ( <. y , z >. e. |^|_ x e. A ( C X. B ) <-> A. x e. A <. y , z >. e. ( C X. B ) ) )
20 18 19 ax-mp 
 |-  ( <. y , z >. e. |^|_ x e. A ( C X. B ) <-> A. x e. A <. y , z >. e. ( C X. B ) )
21 16 17 20 3bitr4g 
 |-  ( A =/= (/) -> ( <. y , z >. e. ( C X. |^|_ x e. A B ) <-> <. y , z >. e. |^|_ x e. A ( C X. B ) ) )
22 21 eqrelrdv2 
 |-  ( ( ( Rel ( C X. |^|_ x e. A B ) /\ Rel |^|_ x e. A ( C X. B ) ) /\ A =/= (/) ) -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )
23 8 22 mpancom 
 |-  ( A =/= (/) -> ( C X. |^|_ x e. A B ) = |^|_ x e. A ( C X. B ) )