Metamath Proof Explorer

Theorem cossidcnvss

Description: A class composed with itself is included in the identity relation and has its range included in its domain if and only if its converse is included in it and it is single-valued. (Contributed by BJ, 8-Nov-2026)

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

Proof

Step Hyp Ref Expression
1 bj-cnvresrn 
 |-  ( `' B |` ran B ) = `' B
2 simpr 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ran B C_ dom B )
3 ssres2 
 |-  ( ran B C_ dom B -> ( `' B |` ran B ) C_ ( `' B |` dom B ) )
4 2 3 syl 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( `' B |` ran B ) C_ ( `' B |` dom B ) )
5 simpl 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( B o. B ) C_ _I )
6 cossidres2 
 |-  ( ( B o. B ) C_ _I -> ( `' B |` dom B ) C_ B )
7 5 6 syl 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( `' B |` dom B ) C_ B )
8 4 7 sstrd 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( `' B |` ran B ) C_ B )
9 1 8 eqsstrrid 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> `' B C_ B )
10 coss2 
 |-  ( `' B C_ B -> ( B o. `' B ) C_ ( B o. B ) )
11 9 10 syl 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( B o. `' B ) C_ ( B o. B ) )
12 11 5 sstrd 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( B o. `' B ) C_ _I )
13 9 12 jca 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) -> ( `' B C_ B /\ ( B o. `' B ) C_ _I ) )
14 cocnvcnv2 
 |-  ( B o. `' `' B ) = ( B o. B )
15 simpl 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> `' B C_ B )
16 cnvss 
 |-  ( `' B C_ B -> `' `' B C_ `' B )
17 15 16 syl 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> `' `' B C_ `' B )
18 coss2 
 |-  ( `' `' B C_ `' B -> ( B o. `' `' B ) C_ ( B o. `' B ) )
19 17 18 syl 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ( B o. `' `' B ) C_ ( B o. `' B ) )
20 simpr 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ( B o. `' B ) C_ _I )
21 19 20 sstrd 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ( B o. `' `' B ) C_ _I )
22 14 21 eqsstrrid 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ( B o. B ) C_ _I )
23 df-rn 
 |-  ran B = dom `' B
24 dmss 
 |-  ( `' B C_ B -> dom `' B C_ dom B )
25 15 24 syl 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> dom `' B C_ dom B )
26 23 25 eqsstrid 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ran B C_ dom B )
27 22 26 jca 
 |-  ( ( `' B C_ B /\ ( B o. `' B ) C_ _I ) -> ( ( B o. B ) C_ _I /\ ran B C_ dom B ) )
28 13 27 impbii 
 |-  ( ( ( B o. B ) C_ _I /\ ran B C_ dom B ) <-> ( `' B C_ B /\ ( B o. `' B ) C_ _I ) )