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. suceqd
70. suceq
71. elsuci
72. elsucg
73. elsuc2g
74. elsuc
75. elsuc2
76. nfsuc
77. elelsuc
78. sucel
79. suc0
80. sucprc
81. unisucs
82. unisucg
83. unisuc
84. sssucid
85. sucidg
86. sucid
87. nsuceq0
88. eqelsuc
89. iunsuc
90. suctr
91. trsuc
92. trsucss
93. ordsssuc
94. onsssuc
95. ordsssuc2
96. onmindif
97. ordnbtwn
98. onnbtwn
99. sucssel
100. orddif
101. orduniss
102. ordtri2or
103. ordtri2or2
104. ordtri2or3
105. ordelinel
106. ordssun
107. ordequn
108. ordun
109. onunel
110. ordunisssuc
111. suc11
112. onun2
113. ontr
114. onunisuc
115. onordi
116. ontrciOLD
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