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

Metamath Proof Explorer

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