Theorem cocnv2ssidim

Description: Consequence of the composition of a class with a converse being included in the identity relation. The instance where the two classes are equal expresses single-valuedness. (Contributed by BJ, 24-Oct-2026) Note: can shorten fununiq .

	Ref	Expression
Hypotheses	cocnv2ssidim.1	$$⊢X\in \mathrm{V}$$
	cocnv2ssidim.2	$$⊢Y\in \mathrm{V}$$
	cocnv2ssidim.3	$$⊢Z\in \mathrm{V}$$
Assertion	cocnv2ssidim	$$⊢S\circ R^{-1}\subseteq \mathrm{I}\to \left(\left(XRY\wedge XSZ\right)\to Y=Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		cocnv2ssidim.1	$$⊢X\in \mathrm{V}$$
2		cocnv2ssidim.2	$$⊢Y\in \mathrm{V}$$
3		cocnv2ssidim.3	$$⊢Z\in \mathrm{V}$$
4	2 1	brcnv	$$⊢Y{R}^{-1}X\leftrightarrow XRY$$
5	2 1 3	brcoi	$$⊢\left(Y{R}^{-1}X\wedge XSZ\right)\to Y\left(S\circ R^{-1}\right)Z$$
6	4 5	sylanbr	$$⊢\left(XRY\wedge XSZ\right)\to Y\left(S\circ R^{-1}\right)Z$$
7		ssbr	$$⊢S\circ R^{-1}\subseteq \mathrm{I}\to \left(Y\left(S\circ R^{-1}\right)Z\to Y\mathrm{I}Z\right)$$
8	3	ideq	$$⊢Y\mathrm{I}Z\leftrightarrow Y=Z$$
9	7 8	imbitrdi	$$⊢S\circ R^{-1}\subseteq \mathrm{I}\to \left(Y\left(S\circ R^{-1}\right)Z\to Y=Z\right)$$
10	6 9	syl5	$$⊢S\circ R^{-1}\subseteq \mathrm{I}\to \left(\left(XRY\wedge XSZ\right)\to Y=Z\right)$$