# 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}⋉{S}↾}_{{A}}={R}⋉\left({{S}↾}_{{A}}\right)$

### Proof

Step Hyp Ref Expression
1 resco ${⊢}{\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}={\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{S}↾}_{{A}}\right)$
2 1 ineq2i ${⊢}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}\right)=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{S}↾}_{{A}}\right)\right)$
3 df-xrn ${⊢}{R}⋉{S}=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)$
4 3 reseq1i ${⊢}{{R}⋉{S}↾}_{{A}}={\left(\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)\right)↾}_{{A}}$
5 inres ${⊢}\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}\right)={\left(\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)\right)↾}_{{A}}$
6 4 5 eqtr4i ${⊢}{{R}⋉{S}↾}_{{A}}=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}\right)$
7 df-xrn ${⊢}{R}⋉\left({{S}↾}_{{A}}\right)=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{S}↾}_{{A}}\right)\right)$
8 2 6 7 3eqtr4i ${⊢}{{R}⋉{S}↾}_{{A}}={R}⋉\left({{S}↾}_{{A}}\right)$