Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 dfdm4 
 |-  dom B = ran `' B
2 1 reseq2i 
 |-  ( `' A |` dom B ) = ( `' A |` ran `' B )
3 cnvco 
 |-  `' ( B o. A ) = ( `' A o. `' B )
4 cnvss 
 |-  ( ( B o. A ) C_ _I -> `' ( B o. A ) C_ `' _I )
5 cnvi 
 |-  `' _I = _I
6 4 5 sseqtrdi 
 |-  ( ( B o. A ) C_ _I -> `' ( B o. A ) C_ _I )
7 3 6 eqsstrrid 
 |-  ( ( B o. A ) C_ _I -> ( `' A o. `' B ) C_ _I )
8 cossidres1 
 |-  ( ( `' A o. `' B ) C_ _I -> ( `' A |` ran `' B ) C_ `' `' B )
9 7 8 syl 
 |-  ( ( B o. A ) C_ _I -> ( `' A |` ran `' B ) C_ `' `' B )
10 cnvcnvss 
 |-  `' `' B C_ B
11 9 10 sstrdi 
 |-  ( ( B o. A ) C_ _I -> ( `' A |` ran `' B ) C_ B )
12 2 11 eqsstrid 
 |-  ( ( B o. A ) C_ _I -> ( `' A |` dom B ) C_ B )