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 ) |
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 ) |