Theorem cocnv1ssidim

Description: Consequence of the composition of a converse with a class being included in the identity relation. The instance where the two classes are equal expresses injectivity. (Contributed by BJ, 1-Nov-2026)

	Ref	Expression
Hypotheses	cocnv1ssidim.1	|- X e. _V
	cocnv1ssidim.2	|- Y e. _V
	cocnv1ssidim.3	|- Z e. _V
Assertion	cocnv1ssidim	|- ( ( `' S o. R ) C_ _I -> ( ( X R Y /\ Z S Y ) -> X = Z ) )

Proof

Step	Hyp	Ref	Expression
1		cocnv1ssidim.1	|- X e. _V
2		cocnv1ssidim.2	|- Y e. _V
3		cocnv1ssidim.3	|- Z e. _V
4	2 3	brcnv	|- ( Y `' S Z <-> Z S Y )
5	1 2 3	brcoi	|- ( ( X R Y /\ Y `' S Z ) -> X ( `' S o. R ) Z )
6	4 5	sylan2br	|- ( ( X R Y /\ Z S Y ) -> X ( `' S o. R ) Z )
7		ssbr	|- ( ( `' S o. R ) C_ _I -> ( X ( `' S o. R ) Z -> X _I Z ) )
8	3	ideq	|- ( X _I Z <-> X = Z )
9	7 8	imbitrdi	|- ( ( `' S o. R ) C_ _I -> ( X ( `' S o. R ) Z -> X = Z ) )
10	6 9	syl5	|- ( ( `' S o. R ) C_ _I -> ( ( X R Y /\ Z S Y ) -> X = Z ) )