Theorem cossididres

Description: If a composition is included in the identity relation, then the reverse composition includes the identity relation restricted to the appropriate class. (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	cossididres	$$⊢B\circ A\subseteq \mathrm{I}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({B\upharpoonright }_{\mathrm{ran}A}\right)=\mathrm{ran}A\cap \mathrm{dom}B$$
2		incom	$$⊢\mathrm{ran}A\cap \mathrm{dom}B=\mathrm{dom}B\cap \mathrm{ran}A$$
3	1 2	eqtri	$$⊢\mathrm{dom}\left({B\upharpoonright }_{\mathrm{ran}A}\right)=\mathrm{dom}B\cap \mathrm{ran}A$$
4	3	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({B\upharpoonright }_{\mathrm{ran}A}\right)}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}$$
5		idresdmsscocnv1	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({B\upharpoonright }_{\mathrm{ran}A}\right)}\subseteq {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\circ \left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
6	4 5	eqsstrri	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\circ \left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
7		cossidres1	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}$$
8		cnvss	$$⊢{B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
9	7 8	syl	$$⊢B\circ A\subseteq \mathrm{I}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
10		resss	$$⊢{B\upharpoonright }_{\mathrm{ran}A}\subseteq B$$
11	10	a1i	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq B$$
12	9 11	coss12d	$$⊢B\circ A\subseteq \mathrm{I}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\circ \left({B\upharpoonright }_{\mathrm{ran}A}\right)\subseteq {A^{-1}}^{-1}\circ B$$
13		cocnvcnv1	$$⊢{A^{-1}}^{-1}\circ B=A\circ B$$
14	12 13	sseqtrdi	$$⊢B\circ A\subseteq \mathrm{I}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\circ \left({B\upharpoonright }_{\mathrm{ran}A}\right)\subseteq A\circ B$$
15	6 14	sstrid	$$⊢B\circ A\subseteq \mathrm{I}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B$$