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

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

Metamath Proof Explorer