Metamath Proof Explorer

Theorem iinxp

Description: Indexed intersection of Cartesian products is the Cartesian product of indexed intersections. See also inxp and intxp . (Contributed by Zhi Wang, 30-Oct-2025)

Ref Expression
Assertion iinxp 
|- ( A =/= (/) -> |^|_ x e. A ( B X. C ) = ( |^|_ x e. A B X. |^|_ x e. A C ) )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( B X. C )
2 1 rgenw 
 |-  A. x e. A Rel ( B X. C )
3 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A Rel ( B X. C ) ) -> E. x e. A Rel ( B X. C ) )
4 2 3 mpan2 
 |-  ( A =/= (/) -> E. x e. A Rel ( B X. C ) )
5 reliin 
 |-  ( E. x e. A Rel ( B X. C ) -> Rel |^|_ x e. A ( B X. C ) )
6 4 5 syl 
 |-  ( A =/= (/) -> Rel |^|_ x e. A ( B X. C ) )
7 relxp 
 |-  Rel ( |^|_ x e. A B X. |^|_ x e. A C )
8 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
9 8 elv 
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
10 eliin 
 |-  ( z e. _V -> ( z e. |^|_ x e. A C <-> A. x e. A z e. C ) )
11 10 elv 
 |-  ( z e. |^|_ x e. A C <-> A. x e. A z e. C )
12 9 11 anbi12i 
 |-  ( ( y e. |^|_ x e. A B /\ z e. |^|_ x e. A C ) <-> ( A. x e. A y e. B /\ A. x e. A z e. C ) )
13 opelxp 
 |-  ( <. y , z >. e. ( |^|_ x e. A B X. |^|_ x e. A C ) <-> ( y e. |^|_ x e. A B /\ z e. |^|_ x e. A C ) )
14 opex 
 |-  <. y , z >. e. _V
15 eliin 
 |-  ( <. y , z >. e. _V -> ( <. y , z >. e. |^|_ x e. A ( B X. C ) <-> A. x e. A <. y , z >. e. ( B X. C ) ) )
16 14 15 ax-mp 
 |-  ( <. y , z >. e. |^|_ x e. A ( B X. C ) <-> A. x e. A <. y , z >. e. ( B X. C ) )
17 opelxp 
 |-  ( <. y , z >. e. ( B X. C ) <-> ( y e. B /\ z e. C ) )
18 17 ralbii 
 |-  ( A. x e. A <. y , z >. e. ( B X. C ) <-> A. x e. A ( y e. B /\ z e. C ) )
19 r19.26 
 |-  ( A. x e. A ( y e. B /\ z e. C ) <-> ( A. x e. A y e. B /\ A. x e. A z e. C ) )
20 16 18 19 3bitri 
 |-  ( <. y , z >. e. |^|_ x e. A ( B X. C ) <-> ( A. x e. A y e. B /\ A. x e. A z e. C ) )
21 12 13 20 3bitr4ri 
 |-  ( <. y , z >. e. |^|_ x e. A ( B X. C ) <-> <. y , z >. e. ( |^|_ x e. A B X. |^|_ x e. A C ) )
22 21 eqrelriv 
 |-  ( ( Rel |^|_ x e. A ( B X. C ) /\ Rel ( |^|_ x e. A B X. |^|_ x e. A C ) ) -> |^|_ x e. A ( B X. C ) = ( |^|_ x e. A B X. |^|_ x e. A C ) )
23 6 7 22 sylancl 
 |-  ( A =/= (/) -> |^|_ x e. A ( B X. C ) = ( |^|_ x e. A B X. |^|_ x e. A C ) )