Metamath Proof Explorer

Table of Contents - 2.3.13. Ordinals

1. word
2. con0
3. wlim
4. csuc
5. df-ord
6. df-on
7. df-lim
8. df-suc
9. ordeq
10. elong
11. elon
12. eloni
13. elon2
14. limeq
15. ordwe
16. ordtr
17. ordfr
18. ordelss
19. trssord
20. ordirr
21. nordeq
22. ordn2lp
23. tz7.5
24. ordelord
25. tron
26. ordelon
27. onelon
28. tz7.7
29. ordelssne
30. ordelpss
31. ordsseleq
32. ordin
33. onin
34. ordtri3or
35. ordtri1
36. ontri1
37. ordtri2
38. ordtri3
39. ordtri4
40. orddisj
41. onfr
42. onelpss
43. onsseleq
44. onelss
45. ordtr1
46. ordtr2
47. ordtr3
48. ontr1
49. ontr2
50. ordunidif
51. ordintdif
52. onintss
53. oneqmini
54. ord0
55. 0elon
56. ord0eln0
57. on0eln0
58. dflim2
59. inton
60. nlim0
61. limord
62. limuni
63. limuni2
64. 0ellim
65. limelon
66. onn0
67. suceq
68. elsuci
69. elsucg
70. elsuc2g
71. elsuc
72. elsuc2
73. nfsuc
74. elelsuc
75. sucel
76. suc0
77. sucprc
78. unisuc
79. sssucid
80. sucidg
81. sucid
82. nsuceq0
83. eqelsuc
84. iunsuc
85. suctr
86. trsuc
87. trsucss
88. ordsssuc
89. onsssuc
90. ordsssuc2
91. onmindif
92. ordnbtwn
93. onnbtwn
94. sucssel
95. orddif
96. orduniss
97. ordtri2or
98. ordtri2or2
99. ordtri2or3
100. ordelinel
101. ordssun
102. ordequn
103. ordun
104. ordunisssuc
105. suc11
106. onordi
107. ontrci
108. onirri
109. oneli
110. onelssi
111. onssneli
112. onssnel2i
113. onelini
114. oneluni
115. onunisuci
116. onsseli
117. onun2i
118. unizlim
119. on0eqel
120. snsn0non
121. onxpdisj
122. onnev