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∈AB=⋂x∈AC×B

Proof

Step Hyp Ref Expression
1 relxp ⊢Rel⁡C×B
2 1 rgenw ⊢∀x∈ARel⁡C×B
3 r19.2z ⊢A≠∅∧∀x∈ARel⁡C×B→∃x∈ARel⁡C×B
4 2 3 mpan2 ⊢A≠∅→∃x∈ARel⁡C×B
5 reliin ⊢∃x∈ARel⁡C×B→Rel⁡⋂x∈AC×B
6 4 5 syl ⊢A≠∅→Rel⁡⋂x∈AC×B
7 relxp ⊢Rel⁡C×⋂x∈AB
8 6 7 jctil ⊢A≠∅→Rel⁡C×⋂x∈AB∧Rel⁡⋂x∈AC×B
9 r19.28zv ⊢A≠∅→∀x∈Ay∈C∧z∈B↔y∈C∧∀x∈Az∈B
10 9 bicomd ⊢A≠∅→y∈C∧∀x∈Az∈B↔∀x∈Ay∈C∧z∈B
11 eliin ⊢z∈V→z∈⋂x∈AB↔∀x∈Az∈B
12 11 elv ⊢z∈⋂x∈AB↔∀x∈Az∈B
13 12 anbi2i ⊢y∈C∧z∈⋂x∈AB↔y∈C∧∀x∈Az∈B
14 opelxp ⊢yz∈C×B↔y∈C∧z∈B
15 14 ralbii ⊢∀x∈Ayz∈C×B↔∀x∈Ay∈C∧z∈B
16 10 13 15 3bitr4g ⊢A≠∅→y∈C∧z∈⋂x∈AB↔∀x∈Ayz∈C×B
17 opelxp ⊢yz∈C×⋂x∈AB↔y∈C∧z∈⋂x∈AB
18 opex ⊢yz∈V
19 eliin ⊢yz∈V→yz∈⋂x∈AC×B↔∀x∈Ayz∈C×B
20 18 19 ax-mp ⊢yz∈⋂x∈AC×B↔∀x∈Ayz∈C×B
21 16 17 20 3bitr4g ⊢A≠∅→yz∈C×⋂x∈AB↔yz∈⋂x∈AC×B
22 21 eqrelrdv2 ⊢Rel⁡C×⋂x∈AB∧Rel⁡⋂x∈AC×B∧A≠∅→C×⋂x∈AB=⋂x∈AC×B
23 8 22 mpancom ⊢A≠∅→C×⋂x∈AB=⋂x∈AC×B