This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≼ ω \land Fun F) \to F [A] ≼ ω$

Step	Hyp	Ref	Expression
1		ctex	$⊢ A ≼ ω \to A \in V$
2		imadomg	$⊢ A \in V \to (Fun F \to F [A] ≼ A)$
3	2	imp	$⊢ (A \in V \land Fun F) \to F [A] ≼ A$
4	1 3	sylan	$⊢ (A ≼ ω \land Fun F) \to F [A] ≼ A$
5		simpl	$⊢ (A ≼ ω \land Fun F) \to A ≼ ω$
6		domtr	$⊢ (F [A] ≼ A \land A ≼ ω) \to F [A] ≼ ω$
7	4 5 6	syl2anc	$⊢ (A ≼ ω \land Fun F) \to F [A] ≼ ω$