Metamath Proof Explorer


Table of Contents - 2.4.9. The support of functions

In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval) are based on the Axiom of Union (usage of dmexg), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (see suppimacnv). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now).

  1. csupp
  2. df-supp
  3. suppval
  4. supp0prc
  5. suppvalbr
  6. supp0
  7. suppval1
  8. suppvalfn
  9. elsuppfn
  10. cnvimadfsn
  11. suppimacnvss
  12. suppimacnv
  13. frnsuppeq
  14. suppssdm
  15. suppsnop
  16. snopsuppss
  17. fvn0elsupp
  18. fvn0elsuppb
  19. rexsupp
  20. ressuppss
  21. suppun
  22. ressuppssdif
  23. mptsuppdifd
  24. mptsuppd
  25. extmptsuppeq
  26. suppfnss
  27. funsssuppss
  28. fnsuppres
  29. fnsuppeq0
  30. fczsupp0
  31. suppss
  32. suppssr
  33. suppssov1
  34. suppssof1
  35. suppss2
  36. suppsssn
  37. suppssfv
  38. suppofssd
  39. suppofss1d
  40. suppofss2d
  41. suppco
  42. suppcofnd
  43. supp0cosupp0
  44. supp0cosupp0OLD
  45. imacosupp
  46. imacosuppOLD