Theorem cossidres2

Description: If ( B o. A ) is included in the identity relation, then the restriction of the converse of A to the domain of B is included in B . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	cossidres2	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ↾ dom 𝐵 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dfdm4	⊢ dom 𝐵 = ran ◡ 𝐵
2	1	reseq2i	⊢ ( ◡ 𝐴 ↾ dom 𝐵 ) = ( ◡ 𝐴 ↾ ran ◡ 𝐵 )
3		cnvco	⊢ ◡ ( 𝐵 ∘ 𝐴 ) = ( ◡ 𝐴 ∘ ◡ 𝐵 )
4		cnvss	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ◡ ( 𝐵 ∘ 𝐴 ) ⊆ ◡ I )
5		cnvi	⊢ ◡ I = I
6	4 5	sseqtrdi	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ◡ ( 𝐵 ∘ 𝐴 ) ⊆ I )
7	3 6	eqsstrrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ∘ ◡ 𝐵 ) ⊆ I )
8		cossidres1	⊢ ( ( ◡ 𝐴 ∘ ◡ 𝐵 ) ⊆ I → ( ◡ 𝐴 ↾ ran ◡ 𝐵 ) ⊆ ◡ ◡ 𝐵 )
9	7 8	syl	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ↾ ran ◡ 𝐵 ) ⊆ ◡ ◡ 𝐵 )
10		cnvcnvss	⊢ ◡ ◡ 𝐵 ⊆ 𝐵
11	9 10	sstrdi	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ↾ ran ◡ 𝐵 ) ⊆ 𝐵 )
12	2 11	eqsstrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ 𝐴 ↾ dom 𝐵 ) ⊆ 𝐵 )