Metamath Proof Explorer

Table of Contents - 8.3. Examples of categories

1. The category of sets
   1. csetc
   2. df-setc
   3. setcval
   4. setcbas
   5. setchomfval
   6. setchom
   7. elsetchom
   8. setccofval
   9. setcco
   10. setccatid
   11. setccat
   12. setcid
   13. setcmon
   14. setcepi
   15. setcsect
   16. setcinv
   17. setciso
   18. resssetc
   19. funcsetcres2
2. The category of categories
   1. ccatc
   2. df-catc
   3. catcval
   4. catcbas
   5. catchomfval
   6. catchom
   7. catccofval
   8. catcco
   9. catccatid
   10. catcid
   11. catccat
   12. resscatc
   13. catcisolem
   14. catciso
   15. catcoppccl
   16. catcfuccl
3. The category of extensible structures
   1. fncnvimaeqv
   2. bascnvimaeqv
   3. cestrc
   4. df-estrc
   5. estrcval
   6. estrcbas
   7. estrchomfval
   8. estrchom
   9. elestrchom
   10. estrccofval
   11. estrcco
   12. estrcbasbas
   13. estrccatid
   14. estrccat
   15. estrcid
   16. estrchomfn
   17. estrchomfeqhom
   18. estrreslem1
   19. estrreslem2
   20. estrres
   21. funcestrcsetclem1
   22. funcestrcsetclem2
   23. funcestrcsetclem3
   24. funcestrcsetclem4
   25. funcestrcsetclem5
   26. funcestrcsetclem6
   27. funcestrcsetclem7
   28. funcestrcsetclem8
   29. funcestrcsetclem9
   30. funcestrcsetc
   31. fthestrcsetc
   32. fullestrcsetc
   33. equivestrcsetc
   34. setc1strwun
   35. funcsetcestrclem1
   36. funcsetcestrclem2
   37. funcsetcestrclem3
   38. embedsetcestrclem
   39. funcsetcestrclem4
   40. funcsetcestrclem5
   41. funcsetcestrclem6
   42. funcsetcestrclem7
   43. funcsetcestrclem8
   44. funcsetcestrclem9
   45. funcsetcestrc
   46. fthsetcestrc
   47. fullsetcestrc
   48. embedsetcestrc