Metamath Proof Explorer

Table of Contents - 2.4.2. Ordinals (continued)

  1. epweon
  2. ordon
  3. onprc
  4. ssorduni
  5. ssonuni
  6. ssonunii
  7. ordeleqon
  8. ordsson
  9. onss
  10. predon
  11. ssonprc
  12. onuni
  13. orduni
  14. onint
  15. onint0
  16. onssmin
  17. onminesb
  18. onminsb
  19. oninton
  20. onintrab
  21. onintrab2
  22. onnmin
  23. onnminsb
  24. oneqmin
  25. uniordint
  26. onminex
  27. sucon
  28. sucexb
  29. sucexg
  30. sucex
  31. onmindif2
  32. suceloni
  33. ordsuc
  34. ordpwsuc
  35. onpwsuc
  36. sucelon
  37. ordsucss
  38. onpsssuc
  39. ordelsuc
  40. onsucmin
  41. ordsucelsuc
  42. ordsucsssuc
  43. ordsucuniel
  44. ordsucun
  45. ordunpr
  46. ordunel
  47. onsucuni
  48. ordsucuni
  49. orduniorsuc
  50. unon
  51. ordunisuc
  52. orduniss2
  53. onsucuni2
  54. 0elsuc
  55. limon
  56. onssi
  57. onsuci
  58. onuniorsuci
  59. onuninsuci
  60. onsucssi
  61. nlimsucg
  62. orduninsuc
  63. ordunisuc2
  64. ordzsl
  65. onzsl
  66. dflim3
  67. dflim4
  68. limsuc
  69. limsssuc
  70. nlimon
  71. limuni3