Metamath Proof Explorer

Table of Contents - 2.4.15. Functions on ordinals; strictly monotone ordinal functions

1. iunon
2. iinon
3. onfununi
4. onovuni
5. onoviun
6. onnseq
7. wsmo
8. df-smo
9. dfsmo2
10. issmo
11. issmo2
12. smoeq
13. smodm
14. smores
15. smores3
16. smores2
17. smodm2
18. smofvon2
19. iordsmo
20. smo0
21. smofvon
22. smoel
23. smoiun
24. smoiso
25. smoel2
26. smo11
27. smoord
28. smoword
29. smogt
30. smorndom
31. smoiso2