Theorem cossidcnvss2

Description: Two-class version of cossidcnvss . (Contributed by BJ, 8-Nov-2026)

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

Proof

Step	Hyp	Ref	Expression
1		bj-cnvresrn	$$⊢{A^{-1}\upharpoonright }_{\mathrm{ran}A}=A^{-1}$$
2		simpr	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to \mathrm{ran}A\subseteq \mathrm{dom}B$$
3		ssres2	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}B\to {A^{-1}\upharpoonright }_{\mathrm{ran}A}\subseteq {A^{-1}\upharpoonright }_{\mathrm{dom}B}$$
4	2 3	syl	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to {A^{-1}\upharpoonright }_{\mathrm{ran}A}\subseteq {A^{-1}\upharpoonright }_{\mathrm{dom}B}$$
5		simpl	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to B\circ A\subseteq \mathrm{I}$$
6		cossidres2	$$⊢B\circ A\subseteq \mathrm{I}\to {A^{-1}\upharpoonright }_{\mathrm{dom}B}\subseteq B$$
7	5 6	syl	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to {A^{-1}\upharpoonright }_{\mathrm{dom}B}\subseteq B$$
8	4 7	sstrd	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to {A^{-1}\upharpoonright }_{\mathrm{ran}A}\subseteq B$$
9	1 8	eqsstrrid	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to A^{-1}\subseteq B$$
10		relres	$$⊢\mathrm{Rel}\left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
11	10	a1i	$$⊢B\circ A\subseteq \mathrm{I}\to \mathrm{Rel}\left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
12		resss	$$⊢{B\upharpoonright }_{\mathrm{ran}A}\subseteq B$$
13	12	a1i	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq B$$
14		cossidres1	$$⊢B\circ A\subseteq \mathrm{I}\to {B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}$$
15		cnvss	$$⊢{B\upharpoonright }_{\mathrm{ran}A}\subseteq A^{-1}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
16	14 15	syl	$$⊢B\circ A\subseteq \mathrm{I}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq {A^{-1}}^{-1}$$
17		cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$
18	16 17	sstrdi	$$⊢B\circ A\subseteq \mathrm{I}\to {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq A$$
19	13 18	coss12d	$$⊢B\circ A\subseteq \mathrm{I}\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq B\circ A$$
20		id	$$⊢B\circ A\subseteq \mathrm{I}\to B\circ A\subseteq \mathrm{I}$$
21	19 20	sstrd	$$⊢B\circ A\subseteq \mathrm{I}\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq \mathrm{I}$$
22		df-fun	$$⊢\mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\leftrightarrow \left(\mathrm{Rel}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\wedge \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq \mathrm{I}\right)$$
23	11 21 22	sylanbrc	$$⊢B\circ A\subseteq \mathrm{I}\to \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
24	5 23	syl	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
25	9 24	jca	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\to \left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)$$
26		coresrn	$$⊢\left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ A=B\circ A$$
27		cocnvcnv2	$$⊢\left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {A^{-1}}^{-1}=\left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ A$$
28		simpl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to A^{-1}\subseteq B$$
29		ssres	$$⊢A^{-1}\subseteq B\to {A^{-1}\upharpoonright }_{\mathrm{ran}A}\subseteq {B\upharpoonright }_{\mathrm{ran}A}$$
30	28 29	syl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to {A^{-1}\upharpoonright }_{\mathrm{ran}A}\subseteq {B\upharpoonright }_{\mathrm{ran}A}$$
31	1 30	eqsstrrid	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to A^{-1}\subseteq {B\upharpoonright }_{\mathrm{ran}A}$$
32		cnvss	$$⊢A^{-1}\subseteq {B\upharpoonright }_{\mathrm{ran}A}\to {A^{-1}}^{-1}\subseteq {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}$$
33	31 32	syl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to {A^{-1}}^{-1}\subseteq {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}$$
34		coss2	$$⊢{A^{-1}}^{-1}\subseteq {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {A^{-1}}^{-1}\subseteq \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}$$
35	33 34	syl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {A^{-1}}^{-1}\subseteq \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}$$
36		simpr	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)$$
37	22	simprbi	$$⊢\mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq \mathrm{I}$$
38	36 37	syl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {\left({B\upharpoonright }_{\mathrm{ran}A}\right)}^{-1}\subseteq \mathrm{I}$$
39	35 38	sstrd	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ {A^{-1}}^{-1}\subseteq \mathrm{I}$$
40	27 39	eqsstrrid	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \left({B\upharpoonright }_{\mathrm{ran}A}\right)\circ A\subseteq \mathrm{I}$$
41	26 40	eqsstrrid	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to B\circ A\subseteq \mathrm{I}$$
42		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
43		dmss	$$⊢A^{-1}\subseteq B\to \mathrm{dom}{A}^{-1}\subseteq \mathrm{dom}B$$
44	28 43	syl	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \mathrm{dom}{A}^{-1}\subseteq \mathrm{dom}B$$
45	42 44	eqsstrid	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \mathrm{ran}A\subseteq \mathrm{dom}B$$
46	41 45	jca	$$⊢\left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)\to \left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)$$
47	25 46	impbii	$$⊢\left(B\circ A\subseteq \mathrm{I}\wedge \mathrm{ran}A\subseteq \mathrm{dom}B\right)\leftrightarrow \left(A^{-1}\subseteq B\wedge \mathrm{Fun}\left({B\upharpoonright }_{\mathrm{ran}A}\right)\right)$$