Metamath Proof Explorer


Table of Contents - 21.20.5.14. "Singletonization" and tagging

This subsection introduces the "singletonization" and the "tagging" of a class. The singletonization of a class is the class of singletons of elements of that class. It is useful since all nonsingletons are disjoint from it, so one can easily adjoin to it disjoint elements, which is what the tagging does: it adjoins the empty set. This can be used for instance to define the one-point compactification of a topological space. It will be used in the next section to define tuples which work for proper classes.

  1. bj-snsetex
  2. bj-clexab
  3. bj-csngl
  4. df-bj-sngl
  5. bj-sngleq
  6. bj-elsngl
  7. bj-snglc
  8. bj-snglss
  9. bj-0nelsngl
  10. bj-snglinv
  11. bj-snglex
  12. bj-ctag
  13. df-bj-tag
  14. bj-tageq
  15. bj-eltag
  16. bj-0eltag
  17. bj-tagn0
  18. bj-tagss
  19. bj-snglsstag
  20. bj-sngltagi
  21. bj-sngltag
  22. bj-tagci
  23. bj-tagcg
  24. bj-taginv
  25. bj-tagex
  26. bj-xtageq
  27. bj-xtagex