Metamath Proof Explorer

Table of Contents - 21.12.15. Well-founded zero, successor, and limits

  1. cwsuc
  2. cwlim
  3. df-wsuc
  4. df-wlim
  5. wsuceq123
  6. wsuceq1
  7. wsuceq2
  8. wsuceq3
  9. nfwsuc
  10. wlimeq12
  11. wlimeq1
  12. wlimeq2
  13. nfwlim
  14. elwlim
  15. wzel
  16. wsuclem
  17. wsucex
  18. wsuccl
  19. wsuclb
  20. wlimss