Metamath Proof Explorer

Table of Contents - 21.47.1. Increasing sequences and subsequences

1. et-ltneverrefl
2. et-equeucl
3. et-sqrtnegnre
4. ormklocald
5. ormkglobd
6. natlocalincr
7. natglobalincr
8. cupword
9. df-upword
10. upwordnul
11. upwordisword
12. singoutnword
13. singoutnupword
14. upwordsing
15. upwordsseti
16. tworepnotupword
17. upwrdfi