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 ∈ A B = ⋂ x ∈ A C × B

Proof

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