Metamath Proof Explorer

Theorem cossididresb

Description: When B is single-valued (see cocnv2ssid ) and A is injective (see cocnv1ssid ) , the composition ( B o. A ) is included in the identity relation if and only if ( A o. B ) includes the identity relation restricted to ( dom B i^i ran A ) . (Contributed by BJ, 8-Nov-2026)

Ref Expression
Assertion cossididresb 
|- ( ( ( B o. `' B ) C_ _I /\ ( `' A o. A ) C_ _I ) -> ( ( B o. A ) C_ _I <-> ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) ) )

Proof

Step Hyp Ref Expression
1 cossididres 
 |-  ( ( B o. A ) C_ _I -> ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) )
2 cnvss 
 |-  ( ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) -> `' ( _I |` ( dom B i^i ran A ) ) C_ `' ( A o. B ) )
3 cnvresid 
 |-  `' ( _I |` ( dom B i^i ran A ) ) = ( _I |` ( dom B i^i ran A ) )
4 cnvco 
 |-  `' ( A o. B ) = ( `' B o. `' A )
5 2 3 4 3sstr3g 
 |-  ( ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) -> ( _I |` ( dom B i^i ran A ) ) C_ ( `' B o. `' A ) )
6 cossidmid 
 |-  ( ( ( B o. `' B ) C_ _I /\ ( `' A o. A ) C_ _I ) -> ( ( _I |` ( dom B i^i ran A ) ) C_ ( `' B o. `' A ) -> ( B o. A ) C_ _I ) )
7 5 6 syl5 
 |-  ( ( ( B o. `' B ) C_ _I /\ ( `' A o. A ) C_ _I ) -> ( ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) -> ( B o. A ) C_ _I ) )
8 1 7 impbid2 
 |-  ( ( ( B o. `' B ) C_ _I /\ ( `' A o. A ) C_ _I ) -> ( ( B o. A ) C_ _I <-> ( _I |` ( dom B i^i ran A ) ) C_ ( A o. B ) ) )