Theorem xrnres4

Description: Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020)

	Ref	Expression
Assertion	xrnres4	|- ( ( R |X. S ) |` A ) = ( ( R |X. S ) i^i ( A X. ( ran ( R |` A ) X. ran ( S |` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnres3	|- ( ( R |X. S ) |` A ) = ( ( R |` A ) |X. ( S |` A ) )
2		dfres4	|- ( R |` A ) = ( R i^i ( A X. ran ( R |` A ) ) )
3		dfres4	|- ( S |` A ) = ( S i^i ( A X. ran ( S |` A ) ) )
4	2 3	xrneq12i	|- ( ( R |` A ) |X. ( S |` A ) ) = ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) )
5		inxpxrn	|- ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) ) = ( ( R |X. S ) i^i ( A X. ( ran ( R |` A ) X. ran ( S |` A ) ) ) )
6	1 4 5	3eqtri	|- ( ( R |X. S ) |` A ) = ( ( R |X. S ) i^i ( A X. ( ran ( R |` A ) X. ran ( S |` A ) ) ) )