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

Metamath Proof Explorer

Theorem xrnres2

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

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

Proof

Step Hyp Ref Expression
1 resco 
 |-  ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) = ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) )
2 1 ineq2i 
 |-  ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) ) )
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 inres 
 |-  ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) ) = ( ( ( `' ( 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 ) i^i ( ( `' ( 2nd |` ( _V X. _V ) ) o. S ) |` A ) )
7 df-xrn 
 |-  ( R |X. ( S |` A ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. R ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. ( S |` A ) ) )
8 2 6 7 3eqtr4i 
 |-  ( ( R |X. S ) |` A ) = ( R |X. ( S |` A ) )