Metamath Proof Explorer

Table of Contents - 8.2. Arrows (disjointified hom-sets)

1. cdoma
2. ccoda
3. carw
4. choma
5. df-doma
6. df-coda
7. df-homa
8. df-arw
9. homarcl
10. homafval
11. homaf
12. homaval
13. elhoma
14. elhomai
15. elhomai2
16. homarcl2
17. homarel
18. homa1
19. homahom2
20. homahom
21. homadm
22. homacd
23. homadmcd
24. arwval
25. arwrcl
26. arwhoma
27. homarw
28. arwdm
29. arwcd
30. dmaf
31. cdaf
32. arwhom
33. arwdmcd
34. Identity and composition for arrows
    1. cida
    2. ccoa
    3. df-ida
    4. df-coa
    5. idafval
    6. idaval
    7. ida2
    8. idahom
    9. idadm
    10. idacd
    11. idaf
    12. coafval
    13. eldmcoa
    14. dmcoass
    15. homdmcoa
    16. coaval
    17. coa2
    18. coahom
    19. coapm
    20. arwlid
    21. arwrid
    22. arwass