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 𝐵 ) = ∅ )