Metamath Proof Explorer


Table of Contents - 2.3.8. Partial and total orderings

We have not yet defined relations (df-rel), but here we introduce a few related notions we will use to develop ordinals. The class variable is no different from other class variables, but it reminds us that typically it represents what we will later call a "relation".

  1. wpo
  2. wor
  3. df-po
  4. df-so
  5. poss
  6. poeq1
  7. poeq2
  8. nfpo
  9. nfso
  10. pocl
  11. poclOLD
  12. ispod
  13. swopolem
  14. swopo
  15. poirr
  16. potr
  17. po2nr
  18. po3nr
  19. po2ne
  20. po0
  21. pofun
  22. sopo
  23. soss
  24. soeq1
  25. soeq2
  26. sonr
  27. sotr
  28. solin
  29. so2nr
  30. so3nr
  31. sotric
  32. sotrieq
  33. sotrieq2
  34. soasym
  35. sotr2
  36. issod
  37. issoi
  38. isso2i
  39. so0
  40. somo