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