Metamath Proof Explorer

Table of Contents - 15.6. Subsystems of surreals

1. Ordinal numbers
   1. cons
   2. df-ons
   3. elons
   4. onssno
   5. onsno
   6. 0ons
   7. 1ons
   8. elons2
   9. elons2d
   10. sltonold
   11. sltonex
   12. onscutleft
   13. onaddscl
   14. onmulscl
   15. peano2ons
2. Surreal recursive sequences
   1. cseqs
   2. df-seqs
   3. seqsex
   4. seqseq123d
   5. nfseqs
   6. seqsval
   7. noseqex
   8. noseq0
   9. noseqp1
   10. noseqind
   11. noseqinds
   12. noseqssno
   13. noseqno
   14. om2noseq0
   15. om2noseqsuc
   16. om2noseqfo
   17. om2noseqlt
   18. om2noseqlt2
   19. om2noseqf1o
   20. om2noseqiso
   21. om2noseqoi
   22. om2noseqrdg
   23. noseqrdglem
   24. noseqrdgfn
   25. noseqrdg0
   26. noseqrdgsuc
   27. seqsfn
   28. seqs1
   29. seqsp1
3. Natural numbers
   1. cnn0s
   2. cnns
   3. df-n0s
   4. df-nns
   5. n0sex
   6. nnsex
   7. peano5n0s
   8. n0ssno
   9. nnssn0s
   10. nnssno
   11. n0sno
   12. nnsno
   13. n0snod
   14. nnsnod
   15. nnn0s
   16. nnn0sd
   17. 0n0s
   18. peano2n0s
   19. dfn0s2
   20. n0sind
   21. n0scut
   22. n0ons
   23. nnne0s
   24. n0sge0
   25. nnsgt0
   26. elnns
   27. elnns2
   28. n0s0suc
   29. nnsge1
   30. n0addscl
   31. n0mulscl
   32. nnaddscl
   33. nnmulscl
   34. 1n0s
   35. 1nns
   36. peano2nns
   37. n0sbday
   38. n0ssold
   39. nnsrecgt0d
   40. seqn0sfn
   41. eln0s
   42. n0s0m1
   43. n0subs
   44. n0p1nns
   45. dfnns2
   46. nnsind
4. Integers
   1. czs
   2. df-zs
   3. zsex
   4. zssno
   5. zno
   6. znod
   7. elzs
   8. nnzsubs
   9. nnzs
   10. nnzsd
   11. 0zs
   12. n0zs
   13. n0zsd
   14. 1zs
   15. znegscl
   16. znegscld
   17. zaddscl
   18. zaddscld
   19. zsubscld
   20. zmulscld
   21. elzn0s
   22. elzs2
   23. eln0zs
   24. elnnzs
   25. elznns
   26. zn0subs
   27. peano5uzs
   28. uzsind
   29. zsbday
   30. zscut
5. Dyadic fractions
   1. c2s
   2. df-2s
   3. cexps
   4. df-exps
   5. czs12
   6. df-zs12
   7. 1p1e2s
   8. no2times
   9. 2nns
   10. 2sno
   11. 2ne0s
   12. n0seo
   13. zseo
   14. nohalf
   15. expsval
   16. expsnnval
   17. exps0
   18. exps1
   19. expsp1
   20. expscl
   21. expsne0
   22. expsgt0
   23. halfcut
   24. cutpw2
   25. pw2bday
   26. addhalfcut
   27. pw2cut
   28. elzs12
   29. zs12ex
   30. zzs12
   31. zs12bday
6. Real numbers
   1. creno
   2. df-reno
   3. elreno
   4. recut
   5. 0reno
   6. renegscl
   7. readdscl
   8. remulscllem1
   9. remulscllem2
   10. remulscl