Theorem coeq0 6259

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 6250 and coundir 6251 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 6112	. . 3 ⊢ Rel (𝐴 ∘ 𝐵)
2		relrn0 5965	. . 3 ⊢ (Rel (𝐴 ∘ 𝐵) → ((𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ∘ 𝐵) = ∅))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ∘ 𝐵) = ∅)
4		rnco 6255	. . 3 ⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵)
5	4	eqeq1i 2768	. 2 ⊢ (ran (𝐴 ∘ 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅)
6		relres 6006	. . . 4 ⊢ Rel (𝐴 ↾ ran 𝐵)
7		reldm0 5920	. . . 4 ⊢ (Rel (𝐴 ↾ ran 𝐵) → ((𝐴 ↾ ran 𝐵) = ∅ ↔ dom (𝐴 ↾ ran 𝐵) = ∅))
8	6, 7	ax-mp 5	. . 3 ⊢ ((𝐴 ↾ ran 𝐵) = ∅ ↔ dom (𝐴 ↾ ran 𝐵) = ∅)
9		relrn0 5965	. . . 4 ⊢ (Rel (𝐴 ↾ ran 𝐵) → ((𝐴 ↾ ran 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅))
10	6, 9	ax-mp 5	. . 3 ⊢ ((𝐴 ↾ ran 𝐵) = ∅ ↔ ran (𝐴 ↾ ran 𝐵) = ∅)
11		dmres 6013	. . . . 5 ⊢ dom (𝐴 ↾ ran 𝐵) = (ran 𝐵 ∩ dom 𝐴)
12		incom 4163	. . . . 5 ⊢ (ran 𝐵 ∩ dom 𝐴) = (dom 𝐴 ∩ ran 𝐵)
13	11, 12	eqtri 2786	. . . 4 ⊢ dom (𝐴 ↾ ran 𝐵) = (dom 𝐴 ∩ ran 𝐵)
14	13	eqeq1i 2768	. . 3 ⊢ (dom (𝐴 ↾ ran 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
15	8, 10, 14	3bitr3i 304	. 2 ⊢ (ran (𝐴 ↾ ran 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)
16	3, 5, 15	3bitri 300	1 ⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅)

Syntax hints:   ↔ wb 209   = wceq 1570   ∩ cin 3905  ∅c0 4287  dom cdm 5663  ran crn 5664   ↾ cres 5665   ∘ ccom 5667  Rel wrel 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675

This theorem is referenced by:  coemptyd  15018  wrdpmtrlast  33394  diophrw  43473  relexpnul  44387