Theorem ixpint

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

	Ref	Expression
Assertion	ixpint	$$⊢B\ne \varnothing \to \underset{x\in A}{⨉}\bigcap B=\bigcap _{y\in B}\underset{x\in A}{⨉}y$$

Proof

Step	Hyp	Ref	Expression
1		ixpeq2	$$⊢\forall x\in A\bigcap B=\bigcap _{y\in B}y\to \underset{x\in A}{⨉}\bigcap B=\underset{x\in A}{⨉}\bigcap _{y\in B}y$$
2		intiin	$$⊢\bigcap B=\bigcap _{y\in B}y$$
3	2	a1i	$$⊢x\in A\to \bigcap B=\bigcap _{y\in B}y$$
4	1 3	mprg	$$⊢\underset{x\in A}{⨉}\bigcap B=\underset{x\in A}{⨉}\bigcap _{y\in B}y$$
5		ixpiin	$$⊢B\ne \varnothing \to \underset{x\in A}{⨉}\bigcap _{y\in B}y=\bigcap _{y\in B}\underset{x\in A}{⨉}y$$
6	4 5	syl5eq	$$⊢B\ne \varnothing \to \underset{x\in A}{⨉}\bigcap B=\bigcap _{y\in B}\underset{x\in A}{⨉}y$$