Theorem coires2

Description: Postcomposing with a restricted identity relation is the same as corestricting. (Contributed by BJ, 1-Nov-2026)

	Ref	Expression
Assertion	coires2	$$⊢\left({\mathrm{I}\upharpoonright }_B\right)\circ A=A\cap \left(\mathrm{V}\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_B\right)}^{-1}={\mathrm{I}\upharpoonright }_B$$
2	1	coeq1i	$$⊢{\left({\mathrm{I}\upharpoonright }_B\right)}^{-1}\circ {A^{-1}}^{-1}=\left({\mathrm{I}\upharpoonright }_B\right)\circ {A^{-1}}^{-1}$$
3		coires1	$$⊢A^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)={A^{-1}\upharpoonright }_B$$
4	3	cnveqi	$$⊢{\left(A^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)\right)}^{-1}={\left({A^{-1}\upharpoonright }_B\right)}^{-1}$$
5		cnvco	$$⊢{\left(A^{-1}\circ \left({\mathrm{I}\upharpoonright }_B\right)\right)}^{-1}={\left({\mathrm{I}\upharpoonright }_B\right)}^{-1}\circ {A^{-1}}^{-1}$$
6		cnvrescnv	$$⊢{\left({A^{-1}\upharpoonright }_B\right)}^{-1}=A\cap \left(\mathrm{V}\times B\right)$$
7	4 5 6	3eqtr3i	$$⊢{\left({\mathrm{I}\upharpoonright }_B\right)}^{-1}\circ {A^{-1}}^{-1}=A\cap \left(\mathrm{V}\times B\right)$$
8		cocnvcnv2	$$⊢\left({\mathrm{I}\upharpoonright }_B\right)\circ {A^{-1}}^{-1}=\left({\mathrm{I}\upharpoonright }_B\right)\circ A$$
9	2 7 8	3eqtr3ri	$$⊢\left({\mathrm{I}\upharpoonright }_B\right)\circ A=A\cap \left(\mathrm{V}\times B\right)$$