Metamath Proof Explorer

Table of Contents - 2.6.2. Existence of omega (the set of natural numbers)

1. omex
2. axinf
3. inf5
4. omelon
5. dfom3
6. elom3
7. dfom4
8. dfom5
9. oancom
10. isfinite
11. fict
12. nnsdom
13. omenps
14. omensuc
15. infdifsn
16. infdiffi
17. unbnn3
18. noinfep