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

Metamath Proof Explorer

Theorem xrninxp

Description: Intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 7-Apr-2020)

Ref Expression
Assertion xrninxp 
|- ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = `' { <. <. y , z >. , u >. | ( ( y e. B /\ z e. C ) /\ ( u e. A /\ u ( R |X. S ) <. y , z >. ) ) }

Proof

Step Hyp Ref Expression
1 inxp2 
 |-  ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = { <. u , x >. | ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) }
2 df-3an 
 |-  ( ( u e. A /\ x e. ( B X. C ) /\ u ( R |X. S ) x ) <-> ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) )
3 3anan12 
 |-  ( ( u e. A /\ x e. ( B X. C ) /\ u ( R |X. S ) x ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) )
4 2 3 bitr3i 
 |-  ( ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) <-> ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) )
5 4 opabbii 
 |-  { <. u , x >. | ( ( u e. A /\ x e. ( B X. C ) ) /\ u ( R |X. S ) x ) } = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) }
6 1 5 eqtri 
 |-  ( ( 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 ) ) }
7 cnvopab 
 |-  `' { <. x , u >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } = { <. u , x >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) }
8 breq2 
 |-  ( x = <. y , z >. -> ( u ( R |X. S ) x <-> u ( R |X. S ) <. y , z >. ) )
9 8 anbi2d 
 |-  ( x = <. y , z >. -> ( ( u e. A /\ u ( R |X. S ) x ) <-> ( u e. A /\ u ( R |X. S ) <. y , z >. ) ) )
10 9 dfoprab4 
 |-  { <. x , u >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } = { <. <. y , z >. , u >. | ( ( y e. B /\ z e. C ) /\ ( u e. A /\ u ( R |X. S ) <. y , z >. ) ) }
11 10 cnveqi 
 |-  `' { <. x , u >. | ( x e. ( B X. C ) /\ ( u e. A /\ u ( R |X. S ) x ) ) } = `' { <. <. y , z >. , u >. | ( ( y e. B /\ z e. C ) /\ ( u e. A /\ u ( R |X. S ) <. y , z >. ) ) }
12 6 7 11 3eqtr2i 
 |-  ( ( R |X. S ) i^i ( A X. ( B X. C ) ) ) = `' { <. <. y , z >. , u >. | ( ( y e. B /\ z e. C ) /\ ( u e. A /\ u ( R |X. S ) <. y , z >. ) ) }