Metamath Proof Explorer

Theorem cossidmid

Description: If ( A o. B ) and ( C o. D ) are included in the identity relation and ( B o. C ) includes it on ( dom A i^i ran D ) , then ( A o. D ) is included in the identity relation. (Contributed by BJ, 8-Nov-2026)

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

Proof

Step Hyp Ref Expression
1 coidmid 
 |-  ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( A o. D ) C_ ( ( A o. B ) o. ( C o. D ) ) )
2 simpl 
 |-  ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) -> ( A o. B ) C_ _I )
3 simpr 
 |-  ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) -> ( C o. D ) C_ _I )
4 2 3 coss12d 
 |-  ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) -> ( ( A o. B ) o. ( C o. D ) ) C_ ( _I o. _I ) )
5 reli 
 |-  Rel _I
6 coi1 
 |-  ( Rel _I -> ( _I o. _I ) = _I )
7 5 6 ax-mp 
 |-  ( _I o. _I ) = _I
8 4 7 sseqtrdi 
 |-  ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) -> ( ( A o. B ) o. ( C o. D ) ) C_ _I )
9 1 8 sylan9ssr 
 |-  ( ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) /\ ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) ) -> ( A o. D ) C_ _I )
10 9 ex 
 |-  ( ( ( A o. B ) C_ _I /\ ( C o. D ) C_ _I ) -> ( ( _I |` ( dom A i^i ran D ) ) C_ ( B o. C ) -> ( A o. D ) C_ _I ) )