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 )