Metamath Proof Explorer

Table of Contents - 21.20.6.9. The canonical bijection from the finite ordinals

1. ciomnn
2. df-bj-iomnn
3. bj-imafv
4. bj-funun
5. bj-fununsn1
6. bj-fununsn2
7. bj-fvsnun1
8. bj-fvsnun2
9. bj-fvmptunsn1
10. bj-fvmptunsn2
11. bj-iomnnom