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

Step	Hyp	Ref	Expression
1		resco	$⊢ {({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ↾}_{A} = {({2^{nd} ↾}_{(V \times V)})}^{-1} \circ ({S ↾}_{A})$
2	1	ineq2i	$⊢ ({({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) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ ({S ↾}_{A}))$
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		inres	$⊢ ({({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) \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) \cap ({({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ↾}_{A})$
7		df-xrn	$⊢ R ⋉ ({S ↾}_{A}) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ ({S ↾}_{A}))$
8	2 6 7	3eqtr4i	$⊢ {R ⋉ S ↾}_{A} = R ⋉ ({S ↾}_{A})$

Metamath Proof Explorer