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	|- ( ( B o. A ) C_ _I -> ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) )

Proof

Step	Hyp	Ref	Expression
1		dmres	|- dom ( B |` ran A ) = ( ran A i^i dom B )
2		incom	|- ( ran A i^i dom B ) = ( dom B i^i ran A )
3	1 2	eqtri	|- dom ( B |` ran A ) = ( dom B i^i ran A )
4	3	reseq2i	|- ( _I |` dom ( B |` ran A ) ) = ( _I |` ( dom B i^i ran A ) )
5		idresdmsscocnv1	|- ( _I |` dom ( B |` ran A ) ) C_ ( `' ( B |` ran A ) o. ( B |` ran A ) )
6	4 5	eqsstrri	|- ( _I |` ( dom B i^i ran A ) ) C_ ( `' ( B |` ran A ) o. ( B |` ran A ) )
7		cossidres1	|- ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ `' A )
8		cnvss	|- ( ( B |` ran A ) C_ `' A -> `' ( B |` ran A ) C_ `' `' A )
9	7 8	syl	|- ( ( B o. A ) C_ _I -> `' ( B |` ran A ) C_ `' `' A )
10		resss	|- ( B |` ran A ) C_ B
11	10	a1i	|- ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ B )
12	9 11	coss12d	|- ( ( B o. A ) C_ _I -> ( `' ( B |` ran A ) o. ( B |` ran A ) ) C_ ( `' `' A o. B ) )
13		cocnvcnv1	|- ( `' `' A o. B ) = ( A o. B )
14	12 13	sseqtrdi	|- ( ( B o. A ) C_ _I -> ( `' ( B |` ran A ) o. ( B |` ran A ) ) C_ ( A o. B ) )
15	6 14	sstrid	|- ( ( B o. A ) C_ _I -> ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) )