Metamath Proof Explorer

Table of Contents - 2.3.14. 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. onelssex
51. ordunidif
52. ordintdif
53. onintss
54. oneqmini
55. ord0
56. 0elon
57. ord0eln0
58. on0eln0
59. dflim2
60. inton
61. nlim0
62. limord
63. limuni
64. limuni2
65. 0ellim
66. limelon
67. onn0
68. suceq
69. elsuci
70. elsucg
71. elsuc2g
72. elsuc
73. elsuc2
74. nfsuc
75. elelsuc
76. sucel
77. suc0
78. sucprc
79. unisucs
80. unisucg
81. unisuc
82. sssucid
83. sucidg
84. sucid
85. nsuceq0
86. eqelsuc
87. iunsuc
88. suctr
89. trsuc
90. trsucss
91. ordsssuc
92. onsssuc
93. ordsssuc2
94. onmindif
95. ordnbtwn
96. onnbtwn
97. sucssel
98. orddif
99. orduniss
100. ordtri2or
101. ordtri2or2
102. ordtri2or3
103. ordelinel
104. ordssun
105. ordequn
106. ordun
107. onunel
108. ordunisssuc
109. suc11
110. onun2
111. ontr
112. onunisuc
113. onordi
114. ontrciOLD
115. onirri
116. oneli
117. onelssi
118. onssneli
119. onssnel2i
120. onelini
121. oneluni
122. onunisuci
123. onsseli
124. onun2i
125. unizlim
126. on0eqel
127. snsn0non
128. onxpdisj
129. onnev
130. onnevOLD