Metamath Proof Explorer

Theorem coss2b

Description: Postcomposition with an injective class (see cocnv1ssid ) preserves and reflects the subclass relation up to corestriction to its domain. This is a generalization of the fact that injections are left-cancellable. Compare with coss1b . There is no special syntax for corestriction as explained in the comment of df-res . (Contributed by BJ, 24-Oct-2026) TODO: prove cocanss1 from it.

Ref Expression
Hypothesis coss2b.1 
|- ( ph -> ( `' F o. F ) C_ _I )
Assertion coss2b 
|- ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) ) )

Proof

Step Hyp Ref Expression
1 coss2b.1 
 |-  ( ph -> ( `' F o. F ) C_ _I )
2 coss2 
 |-  ( ( F o. H ) C_ ( F o. K ) -> ( `' F o. ( F o. H ) ) C_ ( `' F o. ( F o. K ) ) )
3 coass 
 |-  ( ( `' F o. F ) o. H ) = ( `' F o. ( F o. H ) )
4 iss 
 |-  ( ( `' F o. F ) C_ _I <-> ( `' F o. F ) = ( _I |` dom ( `' F o. F ) ) )
5 1 4 sylib 
 |-  ( ph -> ( `' F o. F ) = ( _I |` dom ( `' F o. F ) ) )
6 dmcocnv1 
 |-  dom ( `' F o. F ) = dom F
7 6 reseq2i 
 |-  ( _I |` dom ( `' F o. F ) ) = ( _I |` dom F )
8 5 7 eqtrdi 
 |-  ( ph -> ( `' F o. F ) = ( _I |` dom F ) )
9 8 coeq1d 
 |-  ( ph -> ( ( `' F o. F ) o. H ) = ( ( _I |` dom F ) o. H ) )
10 coires2 
 |-  ( ( _I |` dom F ) o. H ) = ( H i^i ( _V X. dom F ) )
11 9 10 eqtrdi 
 |-  ( ph -> ( ( `' F o. F ) o. H ) = ( H i^i ( _V X. dom F ) ) )
12 3 11 eqtr3id 
 |-  ( ph -> ( `' F o. ( F o. H ) ) = ( H i^i ( _V X. dom F ) ) )
13 coass 
 |-  ( ( `' F o. F ) o. K ) = ( `' F o. ( F o. K ) )
14 8 coeq1d 
 |-  ( ph -> ( ( `' F o. F ) o. K ) = ( ( _I |` dom F ) o. K ) )
15 coires2 
 |-  ( ( _I |` dom F ) o. K ) = ( K i^i ( _V X. dom F ) )
16 14 15 eqtrdi 
 |-  ( ph -> ( ( `' F o. F ) o. K ) = ( K i^i ( _V X. dom F ) ) )
17 13 16 eqtr3id 
 |-  ( ph -> ( `' F o. ( F o. K ) ) = ( K i^i ( _V X. dom F ) ) )
18 12 17 sseq12d 
 |-  ( ph -> ( ( `' F o. ( F o. H ) ) C_ ( `' F o. ( F o. K ) ) <-> ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) ) )
19 2 18 imbitrid 
 |-  ( ph -> ( ( F o. H ) C_ ( F o. K ) -> ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) ) )
20 coss2 
 |-  ( ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) -> ( F o. ( H i^i ( _V X. dom F ) ) ) C_ ( F o. ( K i^i ( _V X. dom F ) ) ) )
21 cnvrescnv 
 |-  `' ( `' H |` dom F ) = ( H i^i ( _V X. dom F ) )
22 21 coeq2i 
 |-  ( F o. `' ( `' H |` dom F ) ) = ( F o. ( H i^i ( _V X. dom F ) ) )
23 ssid 
 |-  dom F C_ dom F
24 cores2 
 |-  ( dom F C_ dom F -> ( F o. `' ( `' H |` dom F ) ) = ( F o. H ) )
25 23 24 ax-mp 
 |-  ( F o. `' ( `' H |` dom F ) ) = ( F o. H )
26 22 25 eqtr3i 
 |-  ( F o. ( H i^i ( _V X. dom F ) ) ) = ( F o. H )
27 cnvrescnv 
 |-  `' ( `' K |` dom F ) = ( K i^i ( _V X. dom F ) )
28 27 coeq2i 
 |-  ( F o. `' ( `' K |` dom F ) ) = ( F o. ( K i^i ( _V X. dom F ) ) )
29 cores2 
 |-  ( dom F C_ dom F -> ( F o. `' ( `' K |` dom F ) ) = ( F o. K ) )
30 23 29 ax-mp 
 |-  ( F o. `' ( `' K |` dom F ) ) = ( F o. K )
31 28 30 eqtr3i 
 |-  ( F o. ( K i^i ( _V X. dom F ) ) ) = ( F o. K )
32 20 26 31 3sstr3g 
 |-  ( ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) -> ( F o. H ) C_ ( F o. K ) )
33 19 32 impbid1 
 |-  ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> ( H i^i ( _V X. dom F ) ) C_ ( K i^i ( _V X. dom F ) ) ) )