Metamath Proof Explorer

Theorem xrnres

Description: Two ways to express restriction of range Cartesian product, see also xrnres2 , xrnres3 . (Contributed by Peter Mazsa, 5-Jun-2021)

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

Proof

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