Theorem cossidres2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}B=\mathrm{ran}{B}^{-1}$$
2	1	reseq2i	$$⊢{A^{-1}\upharpoonright }_{\mathrm{dom}B}={A^{-1}\upharpoonright }_{\mathrm{ran}{B}^{-1}}$$
3		cnvco	$$⊢{\left(B\circ A\right)}^{-1}=A^{-1}\circ B^{-1}$$
4		cnvss	$$⊢B\circ A\subseteq \mathrm{I}\to {\left(B\circ A\right)}^{-1}\subseteq {\mathrm{I}}^{-1}$$
5		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
6	4 5	sseqtrdi	$$⊢B\circ A\subseteq \mathrm{I}\to {\left(B\circ A\right)}^{-1}\subseteq \mathrm{I}$$
7	3 6	eqsstrrid	$$⊢B\circ A\subseteq \mathrm{I}\to A^{-1}\circ B^{-1}\subseteq \mathrm{I}$$
8		cossidres1	$$⊢A^{-1}\circ B^{-1}\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{ran}{B}^{-1}}\subseteq {B^{-1}}^{-1}$$
9	7 8	syl	$$⊢B\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{ran}{B}^{-1}}\subseteq {B^{-1}}^{-1}$$
10		cnvcnvss	$$⊢{B^{-1}}^{-1}\subseteq B$$
11	9 10	sstrdi	$$⊢B\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{ran}{B}^{-1}}\subseteq B$$
12	2 11	eqsstrid	$$⊢B\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{dom}B}\subseteq B$$