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 ~<_ _om -> ran A ~<_ _om )

Proof

Step Hyp Ref Expression
1 cnvct
 |-  ( A ~<_ _om -> `' A ~<_ _om )
2 dmct
 |-  ( `' A ~<_ _om -> dom `' A ~<_ _om )
3 df-rn
 |-  ran A = dom `' A
4 3 breq1i
 |-  ( ran A ~<_ _om <-> dom `' A ~<_ _om )
5 4 biimpri
 |-  ( dom `' A ~<_ _om -> ran A ~<_ _om )
6 1 2 5 3syl
 |-  ( A ~<_ _om -> ran A ~<_ _om )