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

### Proof

Step Hyp Ref Expression
1 resco ${⊢}{\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)↾}_{{A}}={\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{R}↾}_{{A}}\right)$
2 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)$
3 1 2 ineq12i ${⊢}\left({\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)↾}_{{A}}\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 \left({{R}↾}_{{A}}\right)\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{S}↾}_{{A}}\right)\right)$
4 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)$
5 4 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}}$
6 resindir ${⊢}{\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}}=\left({\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)↾}_{{A}}\right)\cap \left({\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}\right)$
7 5 6 eqtri ${⊢}{{R}⋉{S}↾}_{{A}}=\left({\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {R}\right)↾}_{{A}}\right)\cap \left({\left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ {S}\right)↾}_{{A}}\right)$
8 df-xrn ${⊢}\left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)=\left({\left({{1}^{st}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{R}↾}_{{A}}\right)\right)\cap \left({\left({{2}^{nd}↾}_{\left(\mathrm{V}×\mathrm{V}\right)}\right)}^{-1}\circ \left({{S}↾}_{{A}}\right)\right)$
9 3 7 8 3eqtr4i ${⊢}{{R}⋉{S}↾}_{{A}}=\left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)$