In group theory one learns that there is exactly one trivial group of size 1, namely $\{e\}$. In addition to the axioms of the group theory, this group is uniquely determined by the axiom:
DIM1 $\forall x \forall y. x=y$.
But how do we actually know that $\{e\}$ is a mathematical object, a model of group theory, that a contradiction cannot be derived from the 4 axioms of group theory (which are by assumption consistent) and the additional axiom DIM1?
Is this even possible? Does the proof refer to the consistency of the set theory (which I suppose cannot be proved by Godel's incompleteness theorem)?
Firstly, one learns in group theory that up to isomorphism there is one group of size $1$.
The existence of a group with one element follows from the existence of a set with one element. For such a set $S=\{s\}$ there is exactly one possible group structure and one easily verifies that the axioms of a group hold. Thus, if a set with one element exists, then a group with one element exists. Now, depending on your axioms for set theory, but certainly in $ZF$, you can prove that if a set exists, then a set with one element exists. Thus, if a set exists, then a group with one element exists.