Theorem iinxp

Description: Indexed intersection of Cartesian products is the Cartesian product of indexed intersections. See also inxp and intxp . (Contributed by Zhi Wang, 30-Oct-2025)

	Ref	Expression
Assertion	iinxp	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) = ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) )

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		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
9	8	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
10		eliin	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 ) )
11	10	elv	⊢ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
12	9 11	anbi12i	⊢ ( ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 ) )
13		opelxp	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) ↔ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐶 ) )
14		opex	⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
15		eliin	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ V → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )
16	14 15	ax-mp	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) )
17		opelxp	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
18	17	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
19		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 ) )
20	16 18 19	3bitri	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 ) )
21	12 13 20	3bitr4ri	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) )
22	21	eqrelriv	⊢ ( ( Rel ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ∧ Rel ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) ) → ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) = ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) )
23	6 7 22	sylancl	⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) = ( ∩ 𝑥 ∈ 𝐴 𝐵 × ∩ 𝑥 ∈ 𝐴 𝐶 ) )