Theorem cossidres1

Description: If ( B o. A ) is included in the identity relation, then the restriction of B to the range of A is included in the converse of A . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidres1	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		coires1	$$⊢B\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\right)={B\upharpoonright }_{\mathrm{ran}A}$$
2		idresrnsscocnv2	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\subseteq A\circ A^{-1}$$
3		coss2	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\subseteq A\circ A^{-1}\to B\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\right)\subseteq B\circ \left(A\circ A^{-1}\right)$$
4	2 3	ax-mp	$$⊢B\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\right)\subseteq B\circ \left(A\circ A^{-1}\right)$$
5		coass	$$⊢\left(B\circ A\right)\circ A^{-1}=B\circ \left(A\circ A^{-1}\right)$$
6		coss1	$$⊢B\circ A\subseteq \mathrm{I}\to \left(B\circ A\right)\circ A^{-1}\subseteq \mathrm{I}\circ A^{-1}$$
7		coi2ss	$$⊢\mathrm{I}\circ A^{-1}\subseteq A^{-1}$$
8	6 7	sstrdi	$$⊢B\circ A\subseteq \mathrm{I}\to \left(B\circ A\right)\circ A^{-1}\subseteq A^{-1}$$
9	5 8	eqsstrrid	$$⊢B\circ A\subseteq \mathrm{I}\to B\circ \left(A\circ A^{-1}\right)\subseteq A^{-1}$$
10	4 9	sstrid	$$⊢B\circ A\subseteq \mathrm{I}\to B\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\right)\subseteq A^{-1}$$
11	1 10	eqsstrrid	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}$$