Theorem rnct

Description: The range of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	rnct	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{ran}A\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		cnvct	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\preccurlyeq \mathrm{\omega }$$
2		dmct	$$⊢A^{-1}\preccurlyeq \mathrm{\omega }\to \mathrm{dom}{A}^{-1}\preccurlyeq \mathrm{\omega }$$
3		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
4	3	breq1i	$$⊢\mathrm{ran}A\preccurlyeq \mathrm{\omega }\leftrightarrow \mathrm{dom}{A}^{-1}\preccurlyeq \mathrm{\omega }$$
5	4	biimpri	$$⊢\mathrm{dom}{A}^{-1}\preccurlyeq \mathrm{\omega }\to \mathrm{ran}A\preccurlyeq \mathrm{\omega }$$
6	1 2 5	3syl	$$⊢A\preccurlyeq \mathrm{\omega }\to \mathrm{ran}A\preccurlyeq \mathrm{\omega }$$