Metamath Proof Explorer

Table of Contents - _Begriffsschrift_ Chapter III Member of sequence

means is a member of the -sequence begining with and is a member of the -sequence ending with .

dffrege99 through frege114 develop this.

This will be shown to be related to the transitive-reflexive closure of relation . But more work needs to be done on transitive closure of relations before this is ready for Metamath.

  1. dffrege99
  2. frege100
  3. frege101
  4. frege102
  5. frege103
  6. frege104
  7. frege105
  8. frege106
  9. frege107
  10. frege108
  11. frege109
  12. frege110
  13. frege111
  14. frege112
  15. frege113
  16. frege114