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	⊢ 𝑋 ∈ V
	cocnv1ssidim.2	⊢ 𝑌 ∈ V
	cocnv1ssidim.3	⊢ 𝑍 ∈ V
Assertion	cocnv1ssidim	⊢ ( ( ◡ 𝑆 ∘ 𝑅 ) ⊆ I → ( ( 𝑋 𝑅 𝑌 ∧ 𝑍 𝑆 𝑌 ) → 𝑋 = 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		cocnv1ssidim.1	⊢ 𝑋 ∈ V
2		cocnv1ssidim.2	⊢ 𝑌 ∈ V
3		cocnv1ssidim.3	⊢ 𝑍 ∈ V
4	2 3	brcnv	⊢ ( 𝑌 ◡ 𝑆 𝑍 ↔ 𝑍 𝑆 𝑌 )
5	1 2 3	brcoi	⊢ ( ( 𝑋 𝑅 𝑌 ∧ 𝑌 ◡ 𝑆 𝑍 ) → 𝑋 ( ◡ 𝑆 ∘ 𝑅 ) 𝑍 )
6	4 5	sylan2br	⊢ ( ( 𝑋 𝑅 𝑌 ∧ 𝑍 𝑆 𝑌 ) → 𝑋 ( ◡ 𝑆 ∘ 𝑅 ) 𝑍 )
7		ssbr	⊢ ( ( ◡ 𝑆 ∘ 𝑅 ) ⊆ I → ( 𝑋 ( ◡ 𝑆 ∘ 𝑅 ) 𝑍 → 𝑋 I 𝑍 ) )
8	3	ideq	⊢ ( 𝑋 I 𝑍 ↔ 𝑋 = 𝑍 )
9	7 8	imbitrdi	⊢ ( ( ◡ 𝑆 ∘ 𝑅 ) ⊆ I → ( 𝑋 ( ◡ 𝑆 ∘ 𝑅 ) 𝑍 → 𝑋 = 𝑍 ) )
10	6 9	syl5	⊢ ( ( ◡ 𝑆 ∘ 𝑅 ) ⊆ I → ( ( 𝑋 𝑅 𝑌 ∧ 𝑍 𝑆 𝑌 ) → 𝑋 = 𝑍 ) )