Theorem ixpiin

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

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

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	|- ( B =/= (/) -> ( A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) ) )
2		eliin	|- ( f e. _V -> ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B f e. X_ x e. A C ) )
3	2	elv	|- ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B f e. X_ x e. A C )
4		vex	|- f e. _V
5	4	elixp	|- ( f e. X_ x e. A C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. C ) )
6	5	ralbii	|- ( A. y e. B f e. X_ x e. A C <-> A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) )
7	3 6	bitri	|- ( f e. |^|_ y e. B X_ x e. A C <-> A. y e. B ( f Fn A /\ A. x e. A ( f ` x ) e. C ) )
8	4	elixp	|- ( f e. X_ x e. A |^|_ y e. B C <-> ( f Fn A /\ A. x e. A ( f ` x ) e. |^|_ y e. B C ) )
9		fvex	|- ( f ` x ) e. _V
10		eliin	|- ( ( f ` x ) e. _V -> ( ( f ` x ) e. |^|_ y e. B C <-> A. y e. B ( f ` x ) e. C ) )
11	9 10	ax-mp	|- ( ( f ` x ) e. |^|_ y e. B C <-> A. y e. B ( f ` x ) e. C )
12	11	ralbii	|- ( A. x e. A ( f ` x ) e. |^|_ y e. B C <-> A. x e. A A. y e. B ( f ` x ) e. C )
13		ralcom	|- ( A. x e. A A. y e. B ( f ` x ) e. C <-> A. y e. B A. x e. A ( f ` x ) e. C )
14	12 13	bitri	|- ( A. x e. A ( f ` x ) e. |^|_ y e. B C <-> A. y e. B A. x e. A ( f ` x ) e. C )
15	14	anbi2i	|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. |^|_ y e. B C ) <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) )
16	8 15	bitri	|- ( f e. X_ x e. A |^|_ y e. B C <-> ( f Fn A /\ A. y e. B A. x e. A ( f ` x ) e. C ) )
17	1 7 16	3bitr4g	|- ( B =/= (/) -> ( f e. |^|_ y e. B X_ x e. A C <-> f e. X_ x e. A |^|_ y e. B C ) )
18	17	eqrdv	|- ( B =/= (/) -> |^|_ y e. B X_ x e. A C = X_ x e. A |^|_ y e. B C )
19	18	eqcomd	|- ( B =/= (/) -> X_ x e. A |^|_ y e. B C = |^|_ y e. B X_ x e. A C )