Metamath Proof Explorer

Table of Contents - 2.4.16. "Strong" transfinite recursion

  1. crecs
  2. df-recs
  3. dfrecs3
  4. recseq
  5. nfrecs
  6. tfrlem1
  7. tfrlem3a
  8. tfrlem3
  9. tfrlem4
  10. tfrlem5
  11. recsfval
  12. tfrlem6
  13. tfrlem7
  14. tfrlem8
  15. tfrlem9
  16. tfrlem9a
  17. tfrlem10
  18. tfrlem11
  19. tfrlem12
  20. tfrlem13
  21. tfrlem14
  22. tfrlem15
  23. tfrlem16
  24. tfr1a
  25. tfr2a
  26. tfr2b
  27. tfr1
  28. tfr2
  29. tfr3
  30. tfr1ALT
  31. tfr2ALT
  32. tfr3ALT
  33. recsfnon
  34. recsval
  35. tz7.44lem1
  36. tz7.44-1
  37. tz7.44-2
  38. tz7.44-3