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