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	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{Fun}F\right)\to F\left[A\right]\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
2		imadomg	$$⊢A\in \mathrm{V}\to \left(\mathrm{Fun}F\to F\left[A\right]\preccurlyeq A\right)$$
3	2	imp	$$⊢\left(A\in \mathrm{V}\wedge \mathrm{Fun}F\right)\to F\left[A\right]\preccurlyeq A$$
4	1 3	sylan	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{Fun}F\right)\to F\left[A\right]\preccurlyeq A$$
5		simpl	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{Fun}F\right)\to A\preccurlyeq \mathrm{\omega }$$
6		domtr	$$⊢\left(F\left[A\right]\preccurlyeq A\wedge A\preccurlyeq \mathrm{\omega }\right)\to F\left[A\right]\preccurlyeq \mathrm{\omega }$$
7	4 5 6	syl2anc	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{Fun}F\right)\to F\left[A\right]\preccurlyeq \mathrm{\omega }$$