Metamath Proof Explorer

Theorem cossidcnvss2

Description: Two-class version of cossidcnvss . (Contributed by BJ, 8-Nov-2026)

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

Proof

Step Hyp Ref Expression
1 bj-cnvresrn 
 |-  ( `' A |` ran A ) = `' A
2 simpr 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ran A C_ dom B )
3 ssres2 
 |-  ( ran A C_ dom B -> ( `' A |` ran A ) C_ ( `' A |` dom B ) )
4 2 3 syl 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ( `' A |` ran A ) C_ ( `' A |` dom B ) )
5 simpl 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ( B o. A ) C_ _I )
6 cossidres2 
 |-  ( ( B o. A ) C_ _I -> ( `' A |` dom B ) C_ B )
7 5 6 syl 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ( `' A |` dom B ) C_ B )
8 4 7 sstrd 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ( `' A |` ran A ) C_ B )
9 1 8 eqsstrrid 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> `' A C_ B )
10 relres 
 |-  Rel ( B |` ran A )
11 10 a1i 
 |-  ( ( B o. A ) C_ _I -> Rel ( B |` ran A ) )
12 resss 
 |-  ( B |` ran A ) C_ B
13 12 a1i 
 |-  ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ B )
14 cossidres1 
 |-  ( ( B o. A ) C_ _I -> ( B |` ran A ) C_ `' A )
15 cnvss 
 |-  ( ( B |` ran A ) C_ `' A -> `' ( B |` ran A ) C_ `' `' A )
16 14 15 syl 
 |-  ( ( B o. A ) C_ _I -> `' ( B |` ran A ) C_ `' `' A )
17 cnvcnvss 
 |-  `' `' A C_ A
18 16 17 sstrdi 
 |-  ( ( B o. A ) C_ _I -> `' ( B |` ran A ) C_ A )
19 13 18 coss12d 
 |-  ( ( B o. A ) C_ _I -> ( ( B |` ran A ) o. `' ( B |` ran A ) ) C_ ( B o. A ) )
20 id 
 |-  ( ( B o. A ) C_ _I -> ( B o. A ) C_ _I )
21 19 20 sstrd 
 |-  ( ( B o. A ) C_ _I -> ( ( B |` ran A ) o. `' ( B |` ran A ) ) C_ _I )
22 df-fun 
 |-  ( Fun ( B |` ran A ) <-> ( Rel ( B |` ran A ) /\ ( ( B |` ran A ) o. `' ( B |` ran A ) ) C_ _I ) )
23 11 21 22 sylanbrc 
 |-  ( ( B o. A ) C_ _I -> Fun ( B |` ran A ) )
24 5 23 syl 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> Fun ( B |` ran A ) )
25 9 24 jca 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) -> ( `' A C_ B /\ Fun ( B |` ran A ) ) )
26 coresrn 
 |-  ( ( B |` ran A ) o. A ) = ( B o. A )
27 cocnvcnv2 
 |-  ( ( B |` ran A ) o. `' `' A ) = ( ( B |` ran A ) o. A )
28 simpl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> `' A C_ B )
29 ssres 
 |-  ( `' A C_ B -> ( `' A |` ran A ) C_ ( B |` ran A ) )
30 28 29 syl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( `' A |` ran A ) C_ ( B |` ran A ) )
31 1 30 eqsstrrid 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> `' A C_ ( B |` ran A ) )
32 cnvss 
 |-  ( `' A C_ ( B |` ran A ) -> `' `' A C_ `' ( B |` ran A ) )
33 31 32 syl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> `' `' A C_ `' ( B |` ran A ) )
34 coss2 
 |-  ( `' `' A C_ `' ( B |` ran A ) -> ( ( B |` ran A ) o. `' `' A ) C_ ( ( B |` ran A ) o. `' ( B |` ran A ) ) )
35 33 34 syl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( ( B |` ran A ) o. `' `' A ) C_ ( ( B |` ran A ) o. `' ( B |` ran A ) ) )
36 simpr 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> Fun ( B |` ran A ) )
37 22 simprbi 
 |-  ( Fun ( B |` ran A ) -> ( ( B |` ran A ) o. `' ( B |` ran A ) ) C_ _I )
38 36 37 syl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( ( B |` ran A ) o. `' ( B |` ran A ) ) C_ _I )
39 35 38 sstrd 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( ( B |` ran A ) o. `' `' A ) C_ _I )
40 27 39 eqsstrrid 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( ( B |` ran A ) o. A ) C_ _I )
41 26 40 eqsstrrid 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( B o. A ) C_ _I )
42 df-rn 
 |-  ran A = dom `' A
43 dmss 
 |-  ( `' A C_ B -> dom `' A C_ dom B )
44 28 43 syl 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> dom `' A C_ dom B )
45 42 44 eqsstrid 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ran A C_ dom B )
46 41 45 jca 
 |-  ( ( `' A C_ B /\ Fun ( B |` ran A ) ) -> ( ( B o. A ) C_ _I /\ ran A C_ dom B ) )
47 25 46 impbii 
 |-  ( ( ( B o. A ) C_ _I /\ ran A C_ dom B ) <-> ( `' A C_ B /\ Fun ( B |` ran A ) ) )