Metamath Proof Explorer

Table of Contents - 15.6.1. Ordinal numbers

1. cons
2. df-ons
3. elons
4. onssno
5. onno
6. 0ons
7. 1ons
8. elons2
9. elons2d
10. onleft
11. ltonold
12. ltonsex
13. oncutleft
14. oncutlt
15. bday11on
16. onnolt
17. onlts
18. onles
19. onltsd
20. onlesd
21. oniso
22. onswe
23. onsse
24. onsis
25. ons2ind
26. bdayons
27. onaddscl
28. onmulscl
29. addonbday
30. peano2ons
31. onsbnd
32. onsbnd2