Theorem cossididresb

Description: When B is single-valued (see cocnv2ssid ) and A is injective (see cocnv1ssid ) , the composition ( B o. A ) is included in the identity relation if and only if ( A o. B ) includes the identity relation restricted to ( dom B i^i ran A ) . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossididresb	$$⊢\left(B\circ B^{-1}\subseteq \mathrm{I}\wedge A^{-1}\circ A\subseteq \mathrm{I}\right)\to \left(B\circ A\subseteq \mathrm{I}\leftrightarrow {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cossididres	$$⊢B\circ A\subseteq \mathrm{I}\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B$$
2		cnvss	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B\to {\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\right)}^{-1}\subseteq {\left(A\circ B\right)}^{-1}$$
3		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}$$
4		cnvco	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$
5	2 3 4	3sstr3g	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B\to {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq B^{-1}\circ A^{-1}$$
6		cossidmid	$$⊢\left(B\circ B^{-1}\subseteq \mathrm{I}\wedge A^{-1}\circ A\subseteq \mathrm{I}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq B^{-1}\circ A^{-1}\to B\circ A\subseteq \mathrm{I}\right)$$
7	5 6	syl5	$$⊢\left(B\circ B^{-1}\subseteq \mathrm{I}\wedge A^{-1}\circ A\subseteq \mathrm{I}\right)\to \left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B\to B\circ A\subseteq \mathrm{I}\right)$$
8	1 7	impbid2	$$⊢\left(B\circ B^{-1}\subseteq \mathrm{I}\wedge A^{-1}\circ A\subseteq \mathrm{I}\right)\to \left(B\circ A\subseteq \mathrm{I}\leftrightarrow {\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}B\cap \mathrm{ran}A\right)}\subseteq A\circ B\right)$$