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 >. ) ) }