On the existence of sets in bijection
Given a set $X\not=\emptyset$ is it always true that there is a set $Y$ such as $X\not=Y$ but $X$ and $Y$ are in bijection? I think it is true, but which axioms of logic justify it? I mean, if $X=\{a,b,...\}$ is it enough to say: "let $x,y,...$ elements such that $x\not=a, y\not=b$ etc?" What axiom justifies the existence of such $x,y,$ etc?
Probably the question could be extended: why is there always a couple of different isomorphic groups or rings etc..?
Solution 1:
Neither the Axiom of Choice nor the Axiom of Regularity is needed for this.
Given a set $X,$ define $b=\{x\in X:x\notin x\}.$ It is clear that $b\notin X;$ assuming $b\in X$ leads to the contradiction $b\in b\iff b\notin b.$
If $X\ne\emptyset,$ we can choose an element $a\in X;$ then the set $$Y=(X\setminus\{a\})\cup\{b\}$$ is in bijection with $X,$ and $X\ne Y.$
A similar but slightly more involved argument shows (still without using the Axiom of Choice or the Axiom of Regularity) that, given any set $X,$ we can find a set $Y$ such that $Y$ is in bijection with $X$ and $X\cap Y=\emptyset;$ see this answer.
Now suppose $(G,\cdot)$ is a group. First, we can find a set $H$ which is disjoint from $G$ and in bijection with $G;$ let $f:G\to H$ be a bijection. Then define multiplication on $H$ so that $f$ becomes an isomorphism; namely, for $x,y\in H,$ let $xy=f(f^{-1}(x)f^{-1}(y)).$
Solution 2:
The axiom of choice and it's variant forms effectively make this true. The axiom of choice states that for any well-defined collection of indexed nonempty sets X = {$A_i$|$i\in I$} , there exists a mapping f: $X \rightarrow $$\cup X$ such that f($A_i$) = x where x$\in A_i$. Therefore, it's always possible to define-or "choose"-f in such a way when A,B$\in$ X, f:A$\rightarrow$B is bijective.
One variant of the axiom of choice that give an explicit bijection from X into Y where X,Y $\neq \emptyset$, Tarski's Cartesian product axiom does a great job of this and it's logically equivalent to AOC. Tarski's theorem states that if the Zermelo-Frankel set theory axioms hold, then for every set A, there is a bijective mapping between A and A x A iff AOC is true. The proof-along with the explicit bijection-can be found here. The proof is rather technical, but it's well worth mastering since to my knowledge,it's the only variant of AOC that explicitly gives the bijection.
Get comfortable using AOC, a LOT of higher mathematics relies either explicitly or implicitly upon it.