Metamath references:

* https://us.metamath.org/ileuni/ctinf.html - A set is countably infinite if and only if it has decidable equality, is countable, and is infinite

* https://us.metamath.org/ileuni/qnnen.html - The rational numbers are countably infinite

* https://us.metamath.org/ileuni/ctm.html - Two equivalent definitions of countable for an inhabited set

5/5