Theorem coires1

Description: Precomposing with a restricted identity relation is the same as restricting. (Contributed by FL, 19-Jun-2011) (Revised by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Assertion	coires1	$$⊢A\circ \left({\mathrm{I}\upharpoonright }_B\right)={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		cocnvcnv1	$$⊢{A^{-1}}^{-1}\circ \mathrm{I}=A\circ \mathrm{I}$$
2		relcnv	$$⊢\mathrm{Rel}{A^{-1}}^{-1}$$
3		coi1	$$⊢\mathrm{Rel}{A^{-1}}^{-1}\to {A^{-1}}^{-1}\circ \mathrm{I}={A^{-1}}^{-1}$$
4	2 3	ax-mp	$$⊢{A^{-1}}^{-1}\circ \mathrm{I}={A^{-1}}^{-1}$$
5	1 4	eqtr3i	$$⊢A\circ \mathrm{I}={A^{-1}}^{-1}$$
6	5	reseq1i	$$⊢{\left(A\circ \mathrm{I}\right)\upharpoonright }_B={{A^{-1}}^{-1}\upharpoonright }_B$$
7		resco	$$⊢{\left(A\circ \mathrm{I}\right)\upharpoonright }_B=A\circ \left({\mathrm{I}\upharpoonright }_B\right)$$
8	6 7	eqtr3i	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B=A\circ \left({\mathrm{I}\upharpoonright }_B\right)$$
9		rescnvcnv	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A\upharpoonright }_B$$
10	8 9	eqtr3i	$$⊢A\circ \left({\mathrm{I}\upharpoonright }_B\right)={A\upharpoonright }_B$$