Demonstrate the isomorphism $\text{Perm}(X) \to S_n$ where $X$ is a finite set. Logically, the following is extremely intuitive. However, I am having trouble expressing this in provable form:
Suppose $X$ is a finite set, with $|X|=n$.  Show that,
  given any choice of labeling $X = \{x_1,\ldots, x_n\}$, we get an
  isomorphism $\text{Perm}(X) \to S_n$ given as follows: To $\phi \in
  \text{Perm}(X)$ we associate the permutation $\sigma_\phi \in S_n$ given
  by $\phi(x_i) = x_{\sigma_\phi(i)}$.  That is, show that
  $\sigma_\phi$ is indeed a permutation, and that the map $\text{Perm}(X)
  \to S_n$ is an isomorphism.
 A: Remember that a permutation of a finite set is just a bijective map from this finite set into itself, and that being a bijection is equivalent to being injective and surjective.
Let's show that $\sigma_{\varphi}$ a permutation of $\{1,\ldots,n\}$. Suppose that $\sigma_{\varphi} (i) = \sigma_{\varphi} (j)$. Then $x_{\sigma_{\varphi} (i)} = x_{\sigma_{\varphi} (j)}$ which means that $\varphi(x_i) = \varphi(x_j)$ which means, as $\varphi$ is injective, that $x_i = x_j$ and finally gives $i=j$, showing that $\sigma_{\varphi}$ is injective. Now if $i\in\{1,\ldots,n\}$, then as $\varphi$ is surjective of $X$, we can find an $y\in X$ such that $\varphi(y) = x_i$. By definition of $X$, this $y$ is equal to some $x_j$ for a $j\in \{1,\ldots,n\}$. Then $\varphi(x_j) = x_i$, which means exactly that $\sigma_{\varphi} (j) = i$, showing that $\sigma_{\varphi}$ is surjective. The map $\sigma_{\varphi}$ is a permutation indeed.
For all $i$ you have $x_i = \textrm{Id}(x_i) = x_{\sigma_{\textrm{Id}} (i)} = x_{\textrm{Id}(i)}$ so your map sends $\textrm{Id}$ of $X$ to \textrm{Id} of $\{1,\ldots,n\}$, that is, you have : $\sigma_{\textrm{Id}} = \textrm{Id}$. If $\varphi_1,\varphi_2 \in \textrm{Perm}(X)$, for all $i$ you have $x_{\sigma_{\varphi_1 \circ \varphi_2} (i)} = (\varphi_1 \circ \varphi_2)(x_i) = x_{(\varphi_1 \circ \varphi_2)(i)} = \varphi_1(\varphi_2 (x_i)) = \varphi_1( x_{\sigma_{\varphi_2} (i)} ) = x_{\sigma_{\varphi_1}(\sigma_{\varphi_2} (i))} $ which shows that $\sigma_{\varphi_1 \circ \varphi_2} = \sigma_{\varphi_1}\circ \sigma_{\varphi_2} $. This shows that $\varphi\mapsto \sigma_{\varphi}$ is a group morphism.
I think I can let you finish by showing yourself that $\varphi\mapsto \sigma_{\varphi}$ is an isomorphism ?
A: It might help to clarify everything if you give your labeling function a name. So, let's say we have this function $L: X \to [n] = \{1, 2, \ldots, n\}$ that basically tears the label of each $x_i$ so that $L(x_i) = i$. Now we've got several functions all sharing the same set of domains and codomains ($X$ and $[n]$), so we can use function composition to simplify everything.
Now it's very clear that, given any permutation $\phi \in \text{Perm}(X)$, thinking of $\phi$ as a bijection $X\overset{\phi}{\rightarrow}X$, we can come up with a corresponding bijection $\sigma_\phi: [n] \to [n]$ as follows:
$$ i \overset{L^{-1}}{\longmapsto} x_i \overset{\phi}{\longmapsto} \phi(x_i) = x_j \overset{L}{\longmapsto} j,$$
where, as a composition of bijections, $\sigma_\phi = L^{-1} \circ \phi \circ L : [n] \to [n]$ must be a bijection (that is, element of $S_n$). Let's give this map, which sent the permutation $\phi$ of $X$ to the permutation $\sigma_\phi$ of $[n]$, a name; let's say that $\sigma(\phi) = \sigma_\phi$. Now we need to show that $\sigma : \text{Perm}(X) \to S_n$ is a homomorphism (why is this good enough to automatically be an isomorphism?)
Now you just need to verify that $\sigma(\phi_1\circ\phi_2) = \sigma(\phi_1)\circ\sigma(\phi_2)$, which is very straightforward using function composition and the fact that $\sigma_\phi = L \circ \phi \circ L^{-1}$.
A: This may come late...but why do you not consider the more intuitive direction $$S _n \to S_X$$ where $|X| = n$? Because then it is easy to verify that $$\iota:\begin{cases} S_n \to S_X\\
\sigma \mapsto \begin{pmatrix}x_1 & \dots & x_n\\
x_{\sigma(1)} & \dots & x_{\sigma(n)}
\end{pmatrix}
\end{cases}$$ is a homomorphism and by the obvious injectivity together with the finiteness yields that this is an isomorphism.
