Metamath Proof Explorer


Theorem coeq0

Description: A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi and coundir to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion coeq0
|- ( ( A o. B ) = (/) <-> ( dom A i^i ran B ) = (/) )

Proof

Step Hyp Ref Expression
1 relco
 |-  Rel ( A o. B )
2 relrn0
 |-  ( Rel ( A o. B ) -> ( ( A o. B ) = (/) <-> ran ( A o. B ) = (/) ) )
3 1 2 ax-mp
 |-  ( ( A o. B ) = (/) <-> ran ( A o. B ) = (/) )
4 rnco
 |-  ran ( A o. B ) = ran ( A |` ran B )
5 4 eqeq1i
 |-  ( ran ( A o. B ) = (/) <-> ran ( A |` ran B ) = (/) )
6 relres
 |-  Rel ( A |` ran B )
7 reldm0
 |-  ( Rel ( A |` ran B ) -> ( ( A |` ran B ) = (/) <-> dom ( A |` ran B ) = (/) ) )
8 6 7 ax-mp
 |-  ( ( A |` ran B ) = (/) <-> dom ( A |` ran B ) = (/) )
9 relrn0
 |-  ( Rel ( A |` ran B ) -> ( ( A |` ran B ) = (/) <-> ran ( A |` ran B ) = (/) ) )
10 6 9 ax-mp
 |-  ( ( A |` ran B ) = (/) <-> ran ( A |` ran B ) = (/) )
11 dmres
 |-  dom ( A |` ran B ) = ( ran B i^i dom A )
12 incom
 |-  ( ran B i^i dom A ) = ( dom A i^i ran B )
13 11 12 eqtri
 |-  dom ( A |` ran B ) = ( dom A i^i ran B )
14 13 eqeq1i
 |-  ( dom ( A |` ran B ) = (/) <-> ( dom A i^i ran B ) = (/) )
15 8 10 14 3bitr3i
 |-  ( ran ( A |` ran B ) = (/) <-> ( dom A i^i ran B ) = (/) )
16 3 5 15 3bitri
 |-  ( ( A o. B ) = (/) <-> ( dom A i^i ran B ) = (/) )