Theorem cossididres

Description: If a composition is included in the identity relation, then the reverse composition includes the identity relation restricted to the appropriate class. (Contributed by BJ, 7-Nov-2026)

	Ref	Expression
Assertion	cossididres	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( 𝐵 ↾ ran 𝐴 ) = ( ran 𝐴 ∩ dom 𝐵 )
2		incom	⊢ ( ran 𝐴 ∩ dom 𝐵 ) = ( dom 𝐵 ∩ ran 𝐴 )
3	1 2	eqtri	⊢ dom ( 𝐵 ↾ ran 𝐴 ) = ( dom 𝐵 ∩ ran 𝐴 )
4	3	reseq2i	⊢ ( I ↾ dom ( 𝐵 ↾ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) )
5		idresdmsscocnv1	⊢ ( I ↾ dom ( 𝐵 ↾ ran 𝐴 ) ) ⊆ ( ◡ ( 𝐵 ↾ ran 𝐴 ) ∘ ( 𝐵 ↾ ran 𝐴 ) )
6	4 5	eqsstrri	⊢ ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( ◡ ( 𝐵 ↾ ran 𝐴 ) ∘ ( 𝐵 ↾ ran 𝐴 ) )
7		cossidres1	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 )
8		cnvss	⊢ ( ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ 𝐴 → ◡ ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ ◡ 𝐴 )
9	7 8	syl	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ◡ ( 𝐵 ↾ ran 𝐴 ) ⊆ ◡ ◡ 𝐴 )
10		resss	⊢ ( 𝐵 ↾ ran 𝐴 ) ⊆ 𝐵
11	10	a1i	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( 𝐵 ↾ ran 𝐴 ) ⊆ 𝐵 )
12	9 11	coss12d	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ ( 𝐵 ↾ ran 𝐴 ) ∘ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ ( ◡ ◡ 𝐴 ∘ 𝐵 ) )
13		cocnvcnv1	⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )
14	12 13	sseqtrdi	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( ◡ ( 𝐵 ↾ ran 𝐴 ) ∘ ( 𝐵 ↾ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) )
15	6 14	sstrid	⊢ ( ( 𝐵 ∘ 𝐴 ) ⊆ I → ( I ↾ ( dom 𝐵 ∩ ran 𝐴 ) ) ⊆ ( 𝐴 ∘ 𝐵 ) )