Metamath Proof Explorer

Table of Contents - 2.4.2. Ordinals (continued)

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