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

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

Metamath Proof Explorer