Metamath Proof Explorer

Theorem cossidres1

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

Ref Expression
Assertion cossidres1 
|- ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ `' A )

Proof

Step Hyp Ref Expression
1 coires1 
 |-  ( B o. ( _I |` ran A ) ) = ( B |` ran A )
2 idresrnsscocnv2 
 |-  ( _I |` ran A ) C_ ( A o. `' A )
3 coss2 
 |-  ( ( _I |` ran A ) C_ ( A o. `' A ) -> ( B o. ( _I |` ran A ) ) C_ ( B o. ( A o. `' A ) ) )
4 2 3 ax-mp 
 |-  ( B o. ( _I |` ran A ) ) C_ ( B o. ( A o. `' A ) )
5 coass 
 |-  ( ( B o. A ) o. `' A ) = ( B o. ( A o. `' A ) )
6 coss1 
 |-  ( ( B o. A ) C_ _I -> ( ( B o. A ) o. `' A ) C_ ( _I o. `' A ) )
7 coi2ss 
 |-  ( _I o. `' A ) C_ `' A
8 6 7 sstrdi 
 |-  ( ( B o. A ) C_ _I -> ( ( B o. A ) o. `' A ) C_ `' A )
9 5 8 eqsstrrid 
 |-  ( ( B o. A ) C_ _I -> ( B o. ( A o. `' A ) ) C_ `' A )
10 4 9 sstrid 
 |-  ( ( B o. A ) C_ _I -> ( B o. ( _I |` ran A ) ) C_ `' A )
11 1 10 eqsstrrid 
 |-  ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ `' A )