Theorem coeq0 6207

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 6198 and coundir 6199 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.)

Assertion

Ref	Expression
coeq0	⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)

Proof of Theorem coeq0

Step	Hyp	Ref	Expression
1		relco 6060	. . 3 ⊢ Rel (𝐴 ∘ 𝐵)
2		relrn0 5915	. . 3 ⊢ (Rel (𝐴 ∘ 𝐵) → ((𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ∘ 𝐵) = ∅))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ∘ 𝐵) = ∅)
4		rnco 6203	. . 3 ⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
5	4	eqeq1i 2744	. 2 ⊢ (ran (𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅)
6		relres 5957	. . . 4 ⊢ Rel (𝐴 ↾ ran 𝐵)
7		reldm0 5870	. . . 4 ⊢ (Rel (𝐴 ↾ ran 𝐵) → ((𝐴 ↾ ran 𝐵) = ∅ ↔ dom (𝐴 ↾ ran 𝐵) = ∅))
8	6, 7	ax-mp 5	. . 3 ⊢ ((𝐴 ↾ ran 𝐵) = ∅ ↔ dom (𝐴 ↾ ran 𝐵) = ∅)
9		relrn0 5915	. . . 4 ⊢ (Rel (𝐴 ↾ ran 𝐵) → ((𝐴 ↾ ran 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅))
10	6, 9	ax-mp 5	. . 3 ⊢ ((𝐴 ↾ ran 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅)
11		dmres 5964	. . . . 5 ⊢ dom (𝐴 ↾ ran 𝐵) = (ran 𝐵 ∩ dom 𝐴)
12		incom 4138	. . . . 5 ⊢ (ran 𝐵 ∩ dom 𝐴) = (dom 𝐴 ∩ ran 𝐵)
13	11, 12	eqtri 2762	. . . 4 ⊢ dom (𝐴 ↾ ran 𝐵) = (dom 𝐴 ∩ ran 𝐵)
14	13	eqeq1i 2744	. . 3 ⊢ (dom (𝐴 ↾ ran 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
15	8, 10, 14	3bitr3i 302	. 2 ⊢ (ran (𝐴 ↾ ran 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
16	3, 5, 15	3bitri 298	1 ⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)

Syntax hints:   ↔ wb 207   = wceq 1547   ∩ cin 3882  ∅c0 4261  dom cdm 5618  ran crn 5619   ↾ cres 5620   ∘ ccom 5622  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630

This theorem is referenced by:  coemptyd  14932  wrdpmtrlast  33174  diophrw  43208  relexpnul  44122