Metamath Proof Explorer

Theorem inxpxrn

Description: Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020)

Ref Expression
Assertion inxpxrn 
|- ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) = ( ( R |X. S ) i^i ( A X. ( B X. C ) ) )

Proof

Step Hyp Ref Expression
1 xrnrel 
 |-  Rel ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) )
2 relinxp 
 |-  Rel ( ( R |X. S ) i^i ( A X. ( B X. C ) ) )
3 brxrn2 
 |-  ( u e. _V -> ( u ( R |X. S ) x <-> E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) )
4 3 elv 
 |-  ( u ( R |X. S ) x <-> E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) )
5 4 anbi2i 
 |-  ( ( u e. A /\ u ( R |X. S ) x ) <-> ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) )
6 5 anbi2i 
 |-  ( ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
7 xrninxp2 
 |-  ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) }
8 7 brabidgaw 
 |-  ( u ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) x <-> ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) )
9 brxrn2 
 |-  ( u e. _V -> ( u ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) x <-> E. y E. z ( x = <. y , z >. /\ u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) )
10 9 elv 
 |-  ( u ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) x <-> E. y E. z ( x = <. y , z >. /\ u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) )
11 3anass 
 |-  ( ( x = <. y , z >. /\ u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) <-> ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) )
12 11 2exbii 
 |-  ( E. y E. z ( x = <. y , z >. /\ u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) <-> E. y E. z ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) )
13 brinxp2 
 |-  ( u ( R i^i ( A X. B ) ) y <-> ( ( u e. A /\ y e. B ) /\ u R y ) )
14 brinxp2 
 |-  ( u ( S i^i ( A X. C ) ) z <-> ( ( u e. A /\ z e. C ) /\ u S z ) )
15 13 14 anbi12i 
 |-  ( ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) <-> ( ( ( u e. A /\ y e. B ) /\ u R y ) /\ ( ( u e. A /\ z e. C ) /\ u S z ) ) )
16 anan 
 |-  ( ( ( ( u e. A /\ y e. B ) /\ u R y ) /\ ( ( u e. A /\ z e. C ) /\ u S z ) ) <-> ( ( y e. B /\ z e. C ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) )
17 15 16 bitri 
 |-  ( ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) <-> ( ( y e. B /\ z e. C ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) )
18 17 anbi2i 
 |-  ( ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> ( x = <. y , z >. /\ ( ( y e. B /\ z e. C ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) ) )
19 anass 
 |-  ( ( ( x = <. y , z >. /\ ( y e. B /\ z e. C ) ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( x = <. y , z >. /\ ( ( y e. B /\ z e. C ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) ) )
20 eqelb 
 |-  ( ( x = <. y , z >. /\ x e. ( B X. C ) ) <-> ( x = <. y , z >. /\ <. y , z >. e. ( B X. C ) ) )
21 opelxp 
 |-  ( <. y , z >. e. ( B X. C ) <-> ( y e. B /\ z e. C ) )
22 21 anbi2i 
 |-  ( ( x = <. y , z >. /\ <. y , z >. e. ( B X. C ) ) <-> ( x = <. y , z >. /\ ( y e. B /\ z e. C ) ) )
23 20 22 bitr2i 
 |-  ( ( x = <. y , z >. /\ ( y e. B /\ z e. C ) ) <-> ( x = <. y , z >. /\ x e. ( B X. C ) ) )
24 23 anbi1i 
 |-  ( ( ( x = <. y , z >. /\ ( y e. B /\ z e. C ) ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( ( x = <. y , z >. /\ x e. ( B X. C ) ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) )
25 18 19 24 3bitr2i 
 |-  ( ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> ( ( x = <. y , z >. /\ x e. ( B X. C ) ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) )
26 ancom 
 |-  ( ( x = <. y , z >. /\ x e. ( B X. C ) ) <-> ( x e. ( B X. C ) /\ x = <. y , z >. ) )
27 26 anbi1i 
 |-  ( ( ( x = <. y , z >. /\ x e. ( B X. C ) ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( ( x e. ( B X. C ) /\ x = <. y , z >. ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) )
28 anass 
 |-  ( ( ( x e. ( B X. C ) /\ x = <. y , z >. ) /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( x e. ( B X. C ) /\ ( x = <. y , z >. /\ ( u e. A /\ ( u R y /\ u S z ) ) ) ) )
29 25 27 28 3bitri 
 |-  ( ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> ( x e. ( B X. C ) /\ ( x = <. y , z >. /\ ( u e. A /\ ( u R y /\ u S z ) ) ) ) )
30 an12 
 |-  ( ( x = <. y , z >. /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( u e. A /\ ( x = <. y , z >. /\ ( u R y /\ u S z ) ) ) )
31 3anass 
 |-  ( ( x = <. y , z >. /\ u R y /\ u S z ) <-> ( x = <. y , z >. /\ ( u R y /\ u S z ) ) )
32 31 anbi2i 
 |-  ( ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) <-> ( u e. A /\ ( x = <. y , z >. /\ ( u R y /\ u S z ) ) ) )
33 30 32 bitr4i 
 |-  ( ( x = <. y , z >. /\ ( u e. A /\ ( u R y /\ u S z ) ) ) <-> ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) )
34 33 anbi2i 
 |-  ( ( x e. ( B X. C ) /\ ( x = <. y , z >. /\ ( u e. A /\ ( u R y /\ u S z ) ) ) ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
35 29 34 bitri 
 |-  ( ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
36 35 2exbii 
 |-  ( E. y E. z ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> E. y E. z ( x e. ( B X. C ) /\ ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
37 19.42vv 
 |-  ( E. y E. z ( x e. ( B X. C ) /\ ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) <-> ( x e. ( B X. C ) /\ E. y E. z ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
38 19.42vv 
 |-  ( E. y E. z ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) <-> ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) )
39 38 anbi2i 
 |-  ( ( x e. ( B X. C ) /\ E. y E. z ( u e. A /\ ( x = <. y , z >. /\ u R y /\ u S z ) ) ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
40 36 37 39 3bitri 
 |-  ( E. y E. z ( x = <. y , z >. /\ ( u ( R i^i ( A X. B ) ) y /\ u ( S i^i ( A X. C ) ) z ) ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
41 10 12 40 3bitri 
 |-  ( u ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) x <-> ( x e. ( B X. C ) /\ ( u e. A /\ E. y E. z ( x = <. y , z >. /\ u R y /\ u S z ) ) ) )
42 6 8 41 3bitr4ri 
 |-  ( u ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) x <-> u ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) x )
43 1 2 42 eqbrriv 
 |-  ( ( R i^i ( A X. B ) ) |X. ( S i^i ( A X. C ) ) ) = ( ( R |X. S ) i^i ( A X. ( B X. C ) ) )