This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( 𝐴 ∘ 𝐵 )
2 relrn0 ⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ran ( 𝐴 ∘ 𝐵 ) = ∅ ) )
3 1 2 ax-mp ⊢ ( ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ran ( 𝐴 ∘ 𝐵 ) = ∅ )
4 rnco ⊢ ran ( 𝐴 ∘ 𝐵 ) = ran ( 𝐴 ↾ ran 𝐵 )
5 4 eqeq1i ⊢ ( ran ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ran ( 𝐴 ↾ ran 𝐵 ) = ∅ )
6 relres ⊢ Rel ( 𝐴 ↾ ran 𝐵 )
7 reldm0 ⊢ ( Rel ( 𝐴 ↾ ran 𝐵 ) → ( ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ dom ( 𝐴 ↾ ran 𝐵 ) = ∅ ) )
8 6 7 ax-mp ⊢ ( ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ dom ( 𝐴 ↾ ran 𝐵 ) = ∅ )
9 relrn0 ⊢ ( Rel ( 𝐴 ↾ ran 𝐵 ) → ( ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ ran ( 𝐴 ↾ ran 𝐵 ) = ∅ ) )
10 6 9 ax-mp ⊢ ( ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ ran ( 𝐴 ↾ ran 𝐵 ) = ∅ )
11 dmres ⊢ dom ( 𝐴 ↾ ran 𝐵 ) = ( ran 𝐵 ∩ dom 𝐴 )
12 incom ⊢ ( ran 𝐵 ∩ dom 𝐴 ) = ( dom 𝐴 ∩ ran 𝐵 )
13 11 12 eqtri ⊢ dom ( 𝐴 ↾ ran 𝐵 ) = ( dom 𝐴 ∩ ran 𝐵 )
14 13 eqeq1i ⊢ ( dom ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
15 8 10 14 3bitr3i ⊢ ( ran ( 𝐴 ↾ ran 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
16 3 5 15 3bitri ⊢ ( ( 𝐴 ∘ 𝐵 ) = ∅ ↔ ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )