Metamath Proof Explorer

Theorem coidmid

Description: A composition that includes the identity relation on the relevant class can be inserted in the middle of a composition. (Contributed by BJ, 8-Nov-2026)

Ref Expression
Assertion coidmid 
|- ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( A o. D ) C_ ( ( A o. B ) o. ( C o. D ) ) )

Proof

Step Hyp Ref Expression
1 coss2 
 |-  ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( A o. ( _I |` ( dom A i^i ran D ) ) ) C_ ( A o. ( B o. C ) ) )
2 coss1 
 |-  ( ( A o. ( _I |` ( dom A i^i ran D ) ) ) C_ ( A o. ( B o. C ) ) -> ( ( A o. ( _I |` ( dom A i^i ran D ) ) ) o. D ) C_ ( ( A o. ( B o. C ) ) o. D ) )
3 1 2 syl 
 |-  ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( ( A o. ( _I |` ( dom A i^i ran D ) ) ) o. D ) C_ ( ( A o. ( B o. C ) ) o. D ) )
4 coires1 
 |-  ( A o. ( _I |` ( dom A i^i ran D ) ) ) = ( A |` ( dom A i^i ran D ) )
5 incom 
 |-  ( dom A i^i ran D ) = ( ran D i^i dom A )
6 5 reseq2i 
 |-  ( A |` ( dom A i^i ran D ) ) = ( A |` ( ran D i^i dom A ) )
7 resindm 
 |-  ( A |` ( ran D i^i dom A ) ) = ( A |` ran D )
8 6 7 eqtri 
 |-  ( A |` ( dom A i^i ran D ) ) = ( A |` ran D )
9 4 8 eqtri 
 |-  ( A o. ( _I |` ( dom A i^i ran D ) ) ) = ( A |` ran D )
10 9 coeq1i 
 |-  ( ( A o. ( _I |` ( dom A i^i ran D ) ) ) o. D ) = ( ( A |` ran D ) o. D )
11 coresrn 
 |-  ( ( A |` ran D ) o. D ) = ( A o. D )
12 10 11 eqtri 
 |-  ( ( A o. ( _I |` ( dom A i^i ran D ) ) ) o. D ) = ( A o. D )
13 coass 
 |-  ( ( A o. B ) o. C ) = ( A o. ( B o. C ) )
14 13 coeq1i 
 |-  ( ( ( A o. B ) o. C ) o. D ) = ( ( A o. ( B o. C ) ) o. D )
15 coass 
 |-  ( ( ( A o. B ) o. C ) o. D ) = ( ( A o. B ) o. ( C o. D ) )
16 14 15 eqtr3i 
 |-  ( ( A o. ( B o. C ) ) o. D ) = ( ( A o. B ) o. ( C o. D ) )
17 3 12 16 3sstr3g 
 |-  ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( A o. D ) C_ ( ( A o. B ) o. ( C o. D ) ) )