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