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⋉S\upharpoonright }_A=\left({R\upharpoonright }_A\right)⋉S$$

Proof

Step	Hyp	Ref	Expression
1		resco	$$⊢{\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\upharpoonright }_A={\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left({R\upharpoonright }_A\right)$$
2	1	ineq1i	$$⊢\left({\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\upharpoonright }_A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left({R\upharpoonright }_A\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)$$
3		df-xrn	$$⊢R⋉S=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)$$
4	3	reseq1i	$$⊢{R⋉S\upharpoonright }_A={\left(\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)\right)\upharpoonright }_A$$
5		inres2	$$⊢\left({\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\upharpoonright }_A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)={\left(\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)\right)\upharpoonright }_A$$
6	4 5	eqtr4i	$$⊢{R⋉S\upharpoonright }_A=\left({\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ R\right)\upharpoonright }_A\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)$$
7		df-xrn	$$⊢\left({R\upharpoonright }_A\right)⋉S=\left({\left({1^{st}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ \left({R\upharpoonright }_A\right)\right)\cap \left({\left({2^{nd}\upharpoonright }_{\left(\mathrm{V}\times \mathrm{V}\right)}\right)}^{-1}\circ S\right)$$
8	2 6 7	3eqtr4i	$$⊢{R⋉S\upharpoonright }_A=\left({R\upharpoonright }_A\right)⋉S$$