Images of finitely generated and of finite groups are finitely generated and finite

(Preliminary: images of finite sets.) Let $A$ be a finite set and $f:A\to Y$ any function. The map $\mathrm{\Phi }:f[A]\to \mathcal{P}(A)$, $\mathrm{\Phi }(y):=f^{-1}[\{y\}]$, is injective: for $y\mathrm{\ne }{y}^{\mathrm{\prime }}$ no $a\in A$ has $f(a)=y$ and $f(a)=y^{\mathrm{\prime }}$ simultaneously, so the two preimages are disjoint, and each is nonempty because $y\in f[A]$ [F13]. Hence $\mathrm{\Phi }$ is a bijection from $f[A]$ onto its image, which is a subset of the finite set $\mathcal{P}(A)$ [F11] and therefore finite [F12]; by transport along the bijection, $f[A]$ is finite [F10].

(Words in generators.) For $S\subseteq G$ let $W(S)$ be the set of elements of $G$ expressible as $s_1^{{\epsilon }_1}\cdots s_k^{{\epsilon }_k}$ with $k\ge 0$, $s_i\in S$, ${\epsilon }_i\in \{1,-1\}$, the empty product for $k=0$ being $e$. Then $W(S)=⟨S⟩$. Indeed $⟨S⟩$ is a subgroup containing $S$ [F3], so by the defining closure conditions it contains $e$, every product of elements of $S$, and every inverse, whence $W(S)\subseteq ⟨S⟩$ [F4]; conversely $W(S)$ contains $S$ and $e$, is closed under multiplication by concatenating words, and is closed under inverses by reversing the word and negating all exponents, so $W(S)$ is a subgroup containing $S$ [F4], and minimality gives $⟨S⟩\subseteq W(S)$ [F3].

(Finite case.) If $G$ is finite, the first isomorphism theorem provides an isomorphism $G\mathrm{/}\ker \phi \to \mathrm{im}\phi$, in particular a bijection [F7, F13]. Since $G$ is finite, the quotient $G\mathrm{/}\ker \phi$ is finite [F9]. By transport along the bijection, $\mathrm{im}\phi$ is finite [F10].

(Images of generated subgroups.) For every $S\subseteq G$ one has $\phi (⟨S⟩)=⟨\phi (S)⟩$. For the inclusion $\supseteq$: $\phi (S)\subseteq \phi (⟨S⟩)$, and $\phi (⟨S⟩)$ is the image of the subgroup $⟨S⟩$, hence a subgroup of $H$ [F8], so minimality gives $⟨\phi (S)⟩\subseteq \phi (⟨S⟩)$ [F3]. For the inclusion $\subseteq$: the elements of $⟨S⟩$ have the word form of step 1.2, and multiplicativity together with inversion gives $\phi (s_1^{{\epsilon }_1}\cdots s_k^{{\epsilon }_k})=\phi (s_1{)}^{{\epsilon }_1}\cdots \phi (s_k{)}^{{\epsilon }_k}$ [F1, F2], an element of $⟨\phi (S)⟩$; hence $\phi (⟨S⟩)\subseteq ⟨\phi (S)⟩$.

(Finitely generated case.) If $G$ is finitely generated, fix a finite $S\subseteq G$ with $⟨S⟩=G$ [F5]; this is one existential instantiation, no choice principle is used. Then $\mathrm{im}\phi =\phi (G)=\phi (⟨S⟩)=⟨\phi (S)⟩$ [F6, step 2.1], and $\phi (S)$ is the image of the finite set $S$ under the function $\phi$, hence finite by step 1.1. Therefore $\mathrm{im}\phi$ is generated by the finite set $\phi (S)$ and is finitely generated [F5].

Clause 1 is step 3.1, clause 2 is step 1.3, and the preliminary statement about images of finite sets is step 1.1, so the lemma is proved.