Theorem fimact

Description: The image by a function of a countable set is countable. (Contributed by Thierry Arnoux, 27-Mar-2018)

	Ref	Expression
Assertion	fimact	|- ( ( A ~<_ _om /\ Fun F ) -> ( F " A ) ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		ctex	|- ( A ~<_ _om -> A e. _V )
2		imadomg	|- ( A e. _V -> ( Fun F -> ( F " A ) ~<_ A ) )
3	2	imp	|- ( ( A e. _V /\ Fun F ) -> ( F " A ) ~<_ A )
4	1 3	sylan	|- ( ( A ~<_ _om /\ Fun F ) -> ( F " A ) ~<_ A )
5		simpl	|- ( ( A ~<_ _om /\ Fun F ) -> A ~<_ _om )
6		domtr	|- ( ( ( F " A ) ~<_ A /\ A ~<_ _om ) -> ( F " A ) ~<_ _om )
7	4 5 6	syl2anc	|- ( ( A ~<_ _om /\ Fun F ) -> ( F " A ) ~<_ _om )