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