This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )