Metamath Proof Explorer

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 \in V$
		cocnv1ssidim.2	$⊢ Y \in V$
		cocnv1ssidim.3	$⊢ Z \in V$
	Assertion	cocnv1ssidim	$⊢ S^{-1} \circ R \subseteq I \to ((X R Y \land Z S Y) \to X = Z)$

Proof

Step	Hyp	Ref	Expression
1		cocnv1ssidim.1	$⊢ X \in V$
2		cocnv1ssidim.2	$⊢ Y \in V$
3		cocnv1ssidim.3	$⊢ Z \in V$
4	2 3	brcnv	$⊢ Y S^{-1} Z \leftrightarrow Z S Y$
5	1 2 3	brcoi	$⊢ (X R Y \land Y S^{-1} Z) \to X (S^{-1} \circ R) Z$
6	4 5	sylan2br	$⊢ (X R Y \land Z S Y) \to X (S^{-1} \circ R) Z$
7		ssbr	$⊢ S^{-1} \circ R \subseteq I \to (X (S^{-1} \circ R) Z \to X I Z)$
8	3	ideq	$⊢ X I Z \leftrightarrow X = Z$
9	7 8	imbitrdi	$⊢ S^{-1} \circ R \subseteq I \to (X (S^{-1} \circ R) Z \to X = Z)$
10	6 9	syl5	$⊢ S^{-1} \circ R \subseteq I \to ((X R Y \land Z S Y) \to X = Z)$