Metamath Proof Explorer


Table of Contents - 20.10.20. Natural operations on ordinals

  1. cnadd
  2. df-nadd
  3. on2recsfn
  4. on2recsov
  5. on2ind
  6. on3ind
  7. naddfn
  8. naddcllem
  9. naddcl
  10. naddov
  11. naddov2
  12. naddcom
  13. naddid1
  14. naddssim
  15. naddelim
  16. naddel1
  17. naddel2
  18. naddss1
  19. naddss2