Theorem fimact

Description: The image by a function of a countable set is countable. The proof uses imadomnum rather than imadomg , and so does not require ax-ac . (Contributed by Thierry Arnoux, 27-Mar-2018) (Revised by Vincent Gonzalez, 25-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		omelon	|- _om e. On
2	1	a1i	|- ( ( A ~<_ _om /\ Fun F ) -> _om e. On )
3		simpl	|- ( ( A ~<_ _om /\ Fun F ) -> A ~<_ _om )
4		ondomen	|- ( ( _om e. On /\ A ~<_ _om ) -> A e. dom card )
5	2 3 4	syl2anc	|- ( ( A ~<_ _om /\ Fun F ) -> A e. dom card )
6		simpr	|- ( ( A ~<_ _om /\ Fun F ) -> Fun F )
7		imadomnum	|- ( A e. dom card -> ( Fun F -> ( F " A ) ~<_ A ) )
8	5 6 7	sylc	|- ( ( A ~<_ _om /\ Fun F ) -> ( F " A ) ~<_ A )
9		domtr	|- ( ( ( F " A ) ~<_ A /\ A ~<_ _om ) -> ( F " A ) ~<_ _om )
10	8 3 9	syl2anc	|- ( ( A ~<_ _om /\ Fun F ) -> ( F " A ) ~<_ _om )