Metamath Proof Explorer

Table of Contents - 21.38.6.10. _Begriffsschrift_ Chapter III Member of sequence

means is a member of the -sequence beginning 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