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. onsuc
  37. ordsuc
  38. ordpwsuc
  39. onpwsuc
  40. onsucb
  41. ordsucss
  42. onpsssuc
  43. ordelsuc
  44. onsucmin
  45. ordsucelsuc
  46. ordsucsssuc
  47. ordsucuniel
  48. ordsucun
  49. ordunpr
  50. ordunel
  51. onsucuni
  52. ordsucuni
  53. orduniorsuc
  54. unon
  55. ordunisuc
  56. orduniss2
  57. onsucuni2
  58. 0elsuc
  59. limon
  60. onuniorsuc
  61. onssi
  62. onsuci
  63. onuninsuci
  64. onsucssi
  65. nlimsucg
  66. orduninsuc
  67. ordunisuc2
  68. ordzsl
  69. onzsl
  70. dflim3
  71. dflim4
  72. limsuc
  73. limsssuc
  74. nlimon
  75. limuni3