This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnct

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

		Ref	Expression
	Assertion	rnct	$⊢ A ≼ ω \to ran A ≼ ω$

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