The Set Generated by an Element, and Cyclic Groups

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group, and let $h^{n}$, for $h\in G$ and $n\in\mathbb{Z}$, be the integer power.

(i) The set generated by an element. For $g\in G$, the set generated by $g$ is the set of its integer powers,

$$\langle g\rangle=\{g^{n}:n\in\mathbb{Z}\}$$

(a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)).

(ii) Cyclic groups. $G$ is cyclic if $G=\langle g\rangle$ for some $g\in G$; such a $g$ is a generator of $G$.