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

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 ( 𝐴 ≠ ∅ → ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ( 𝐶 × 𝐵 )
2 1 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 Rel ( 𝐶 × 𝐵 )
3 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 Rel ( 𝐶 × 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 Rel ( 𝐶 × 𝐵 ) )
4 2 3 mpan2 ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 Rel ( 𝐶 × 𝐵 ) )
5 reliin ⊢ ( ∃ 𝑥 ∈ 𝐴 Rel ( 𝐶 × 𝐵 ) → Rel ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )
6 4 5 syl ⊢ ( 𝐴 ≠ ∅ → Rel ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )
7 relxp ⊢ Rel ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 )
8 6 7 jctil ⊢ ( 𝐴 ≠ ∅ → ( Rel ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ∧ Rel ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
9 r19.28zv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ) ) )
10 9 bicomd ⊢ ( 𝐴 ≠ ∅ → ( ( 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵 ) ) )
11 eliin ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ) )
12 11 elv ⊢ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
13 12 anbi2i ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ) )
14 opelxp ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵 ) )
15 14 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵 ) )
16 10 13 15 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × 𝐵 ) ) )
17 opelxp ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) )
18 opex ⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
19 eliin ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ V → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × 𝐵 ) ) )
20 18 19 ax-mp ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × 𝐵 ) )
21 16 17 20 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) )
22 21 eqrelrdv2 ⊢ ( ( ( Rel ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) ∧ Rel ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) ) ∧ 𝐴 ≠ ∅ ) → ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )
23 8 22 mpancom ⊢ ( 𝐴 ≠ ∅ → ( 𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( 𝐶 × 𝐵 ) )