Theorem ixpint

Description: The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015)

	Ref	Expression
Assertion	ixpint	⊢ ( 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ixpeq2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 𝑦 → X 𝑥 ∈ 𝐴 ∩ 𝐵 = X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝑦 )
2		intiin	⊢ ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 𝑦
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 𝑦 )
4	1 3	mprg	⊢ X 𝑥 ∈ 𝐴 ∩ 𝐵 = X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝑦
5		ixpiin	⊢ ( 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝑦 = ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝑦 )
6	4 5	eqtrid	⊢ ( 𝐵 ≠ ∅ → X 𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X 𝑥 ∈ 𝐴 𝑦 )