Metamath Proof Explorer


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 )