| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > relco | Structured version Visualization version GIF version | ||
| Description: A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
| Ref | Expression |
|---|---|
| relco | ⊢ Rel (𝐴 ∘ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-co 5694 | . 2 ⊢ (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} | |
| 2 | 1 | relopabiv 5830 | 1 ⊢ Rel (𝐴 ∘ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 ∃wex 1779 class class class wbr 5143 ∘ ccom 5689 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 df-co 5694 |
| This theorem is referenced by: cotrg 6127 cotrgOLD 6128 cotrgOLDOLD 6129 dfco2 6265 resco 6270 coeq0 6275 coiun 6276 cocnvcnv2 6278 cores2 6279 co02 6280 co01 6281 coi1 6282 coass 6285 cossxp 6292 dfpo2 6316 fmptco 7149 cofunexg 7973 dftpos4 8270 ttrcltr 9756 ttrclco 9758 wunco 10773 relexprelg 15077 relexpaddg 15092 imasless 17585 znleval 21573 metustexhalf 24569 fcoinver 32617 fmptcof2 32667 cnvco1 35759 cnvco2 35760 opelco3 35775 txpss3v 35879 sscoid 35914 xrnss3v 38373 cononrel1 43607 cononrel2 43608 coiun1 43665 relexpaddss 43731 brco2f1o 44045 brco3f1o 44046 neicvgnvor 44129 sblpnf 44329 coxp 48744 |
| Copyright terms: Public domain | W3C validator |