Theorem cossidcnvss

Description: A class composed with itself is included in the identity relation and has its range included in its domain if and only if its converse is included in it and it is single-valued. (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidcnvss	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\leftrightarrow \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-cnvresrn	$$⊢{B^{-1}\upharpoonright }_{\mathrm{ran}B}=B^{-1}$$
2		simpr	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to \mathrm{ran}B\subseteq \mathrm{dom}B$$
3		ssres2	$$⊢\mathrm{ran}B\subseteq \mathrm{dom}B\to {B^{-1}\upharpoonright }_{\mathrm{ran}B}\subseteq {B^{-1}\upharpoonright }_{\mathrm{dom}B}$$
4	2 3	syl	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to {B^{-1}\upharpoonright }_{\mathrm{ran}B}\subseteq {B^{-1}\upharpoonright }_{\mathrm{dom}B}$$
5		simpl	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to B\circ B\subseteq \mathrm{I}$$
6		cossidres2	$$⊢B\circ B\subseteq \mathrm{I}\to {B^{-1}\upharpoonright }_{\mathrm{dom}B}\subseteq B$$
7	5 6	syl	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to {B^{-1}\upharpoonright }_{\mathrm{dom}B}\subseteq B$$
8	4 7	sstrd	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to {B^{-1}\upharpoonright }_{\mathrm{ran}B}\subseteq B$$
9	1 8	eqsstrrid	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to B^{-1}\subseteq B$$
10		coss2	$$⊢B^{-1}\subseteq B\to B\circ B^{-1}\subseteq B\circ B$$
11	9 10	syl	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to B\circ B^{-1}\subseteq B\circ B$$
12	11 5	sstrd	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to B\circ B^{-1}\subseteq \mathrm{I}$$
13	9 12	jca	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\to \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$
14		cocnvcnv2	$$⊢B\circ {B^{-1}}^{-1}=B\circ B$$
15		simpl	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to B^{-1}\subseteq B$$
16		cnvss	$$⊢B^{-1}\subseteq B\to {B^{-1}}^{-1}\subseteq B^{-1}$$
17	15 16	syl	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to {B^{-1}}^{-1}\subseteq B^{-1}$$
18		coss2	$$⊢{B^{-1}}^{-1}\subseteq B^{-1}\to B\circ {B^{-1}}^{-1}\subseteq B\circ B^{-1}$$
19	17 18	syl	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to B\circ {B^{-1}}^{-1}\subseteq B\circ B^{-1}$$
20		simpr	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to B\circ B^{-1}\subseteq \mathrm{I}$$
21	19 20	sstrd	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to B\circ {B^{-1}}^{-1}\subseteq \mathrm{I}$$
22	14 21	eqsstrrid	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to B\circ B\subseteq \mathrm{I}$$
23		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
24		dmss	$$⊢B^{-1}\subseteq B\to \mathrm{dom}{B}^{-1}\subseteq \mathrm{dom}B$$
25	15 24	syl	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to \mathrm{dom}{B}^{-1}\subseteq \mathrm{dom}B$$
26	23 25	eqsstrid	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to \mathrm{ran}B\subseteq \mathrm{dom}B$$
27	22 26	jca	$$⊢\left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)\to \left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)$$
28	13 27	impbii	$$⊢\left(B\circ B\subseteq \mathrm{I}\wedge \mathrm{ran}B\subseteq \mathrm{dom}B\right)\leftrightarrow \left(B^{-1}\subseteq B\wedge B\circ B^{-1}\subseteq \mathrm{I}\right)$$