Theorem ixpint

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

	Ref	Expression
Assertion	ixpint	|- ( B =/= (/) -> X_ x e. A |^| B = |^|_ y e. B X_ x e. A y )

Proof

Step	Hyp	Ref	Expression
1		ixpeq2	|- ( A. x e. A |^| B = |^|_ y e. B y -> X_ x e. A |^| B = X_ x e. A |^|_ y e. B y )
2		intiin	|- |^| B = |^|_ y e. B y
3	2	a1i	|- ( x e. A -> |^| B = |^|_ y e. B y )
4	1 3	mprg	|- X_ x e. A |^| B = X_ x e. A |^|_ y e. B y
5		ixpiin	|- ( B =/= (/) -> X_ x e. A |^|_ y e. B y = |^|_ y e. B X_ x e. A y )
6	4 5	eqtrid	|- ( B =/= (/) -> X_ x e. A |^| B = |^|_ y e. B X_ x e. A y )