![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > coeq0 | Unicode version |
Description: A composition of two relations is empty iff there is no overlap betwen the range of the second and the domain of the first. Useful in combination with coundi 5513 and coundir 5514 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Ref | Expression |
---|---|
coeq0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relco 5510 | . . 3 | |
2 | relrn0 5265 | . . 3 | |
3 | 1, 2 | ax-mp 5 | . 2 |
4 | rnco 5518 | . . 3 | |
5 | 4 | eqeq1i 2464 | . 2 |
6 | relres 5306 | . . . 4 | |
7 | reldm0 5225 | . . . 4 | |
8 | 6, 7 | ax-mp 5 | . . 3 |
9 | relrn0 5265 | . . . 4 | |
10 | 6, 9 | ax-mp 5 | . . 3 |
11 | dmres 5299 | . . . . 5 | |
12 | incom 3690 | . . . . 5 | |
13 | 11, 12 | eqtri 2486 | . . . 4 |
14 | 13 | eqeq1i 2464 | . . 3 |
15 | 8, 10, 14 | 3bitr3i 275 | . 2 |
16 | 3, 5, 15 | 3bitri 271 | 1 |
Colors of variables: wff setvar class |
Syntax hints: <-> wb 184 = wceq 1395
i^i cin 3474 c0 3784 dom cdm 5004 ran crn 5005
|` cres 5006 o. ccom 5008 Rel wrel 5009 |
This theorem is referenced by: coeq0i 30686 diophrw 30692 coemptyd 37760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pr 4691 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-sn 4030 df-pr 4032 df-op 4036 df-br 4453 df-opab 4511 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 |
Copyright terms: Public domain | W3C validator |