Metamath Proof Explorer

Table of Contents - 2.4.4. The natural numbers (i.e., finite ordinals)

  1. com
  2. df-om
  3. dfom2
  4. elom
  5. omsson
  6. limomss
  7. nnon
  8. nnoni
  9. nnord
  10. trom
  11. ordom
  12. elnn
  13. omon
  14. omelon2
  15. nnlim
  16. omssnlim
  17. limom
  18. peano2b
  19. nnsuc
  20. omsucne
  21. ssnlim
  22. omsinds
  23. omun