Metamath Proof Explorer

Theorem idresrnsscocnv2

Description: A class precomposed with its converse includes the identity relation restricted to its range. (Contributed by BJ, 25-Oct-2026)

Ref Expression
Assertion idresrnsscocnv2 
|- ( _I |` ran A ) C_ ( A o. `' A )

Proof

Step Hyp Ref Expression
1 idresdmsscocnv1 
 |-  ( _I |` dom `' A ) C_ ( `' `' A o. `' A )
2 df-rn 
 |-  ran A = dom `' A
3 2 eqcomi 
 |-  dom `' A = ran A
4 3 reseq2i 
 |-  ( _I |` dom `' A ) = ( _I |` ran A )
5 cocnvcnv1 
 |-  ( `' `' A o. `' A ) = ( A o. `' A )
6 1 4 5 3sstr3i 
 |-  ( _I |` ran A ) C_ ( A o. `' A )