Theorem rnct

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

	Ref	Expression
Assertion	rnct	⊢ ( 𝐴 ≼ ω → ran 𝐴 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		cnvct	⊢ ( 𝐴 ≼ ω → ◡ 𝐴 ≼ ω )
2		dmct	⊢ ( ◡ 𝐴 ≼ ω → dom ◡ 𝐴 ≼ ω )
3		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
4	3	breq1i	⊢ ( ran 𝐴 ≼ ω ↔ dom ◡ 𝐴 ≼ ω )
5	4	biimpri	⊢ ( dom ◡ 𝐴 ≼ ω → ran 𝐴 ≼ ω )
6	1 2 5	3syl	⊢ ( 𝐴 ≼ ω → ran 𝐴 ≼ ω )