Metamath Proof Explorer

Theorem xrnres3

Description: Two ways to express restriction of range Cartesian product, see also xrnres , xrnres2 . (Contributed by Peter Mazsa, 28-Mar-2020)

Ref Expression
Assertion xrnres3 
|- ( ( R |X. S ) |` A ) = ( ( R |` A ) |X. ( S |` A ) )

Proof

Step Hyp Ref Expression
1 resco 
 |-  ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) |` A ) = ( `' ( 1st |` ( _V X. _V ) ) o. ( R |` A ) )
2 resco 
 |-  ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) = ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) )
3 1 2 ineq12i 
 |-  ( ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) |` A ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( R |` A ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) ) )
4 df-xrn 
 |-  ( R |X. S ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) )
5 4 reseq1i 
 |-  ( ( R |X. S ) |` A ) = ( ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) |` A )
6 resindir 
 |-  ( ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. S ) ) |` A ) = ( ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) |` A ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) )
7 5 6 eqtri 
 |-  ( ( R |X. S ) |` A ) = ( ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) |` A ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) )
8 df-xrn 
 |-  ( ( R |` A ) |X. ( S |` A ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. ( R |` A ) ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) ) )
9 3 7 8 3eqtr4i 
 |-  ( ( R |X. S ) |` A ) = ( ( R |` A ) |X. ( S |` A ) )