Help understanding proof about normal subgroup with finite index I partially understand the below proof, but not completely.  I have a few questions that I inserted along the way:
Problem: If a group $G$ has a subgroup $H$ of finite index $n$, then there is a normal subgroup $K$ of $G$ with $K \leq H$ and $|G:K| \leq n!$
Proof. We know that the permutation representation induced by the action of $G$ on the left cosets of $H$ by left multiplication is a homomorphism from $G$ into the symmetric group $S_{G/H} \cong S_{n}$.
(Why exactly are we comparing $S_{G/H}$ and how do we know that such a homomorphism exists?  Does one always exist?)
Then, since the kernel of the homomorphism - call it $K$ - is a subgroup of $H$ (I know this because of a given theorem), and so $K$ is a normal subgroup of $G$ with $K \leq H$. Then, by the first isomorphism theorem, $G/K$ is isomorphic to a subgroup of $S_{n}.$ (What is the significance of this part with being isomorphic to a subgroup of $S_{n}$? I commonly see this fact used in proofs, but I still can't see why we care. It seems kind of vague). Thus, $|G:K|=|G/K| \leq |S_{n}|=n!$.
 A: 
Why exactly are we comparing $S_{G/H}$ and how do we know that such a homomorphism exists? Does one always exist?

This is the general idea of the action of a group on a set. By definition, for a set $X$, the symmetric group $S_X$ is the group of permutations of $X$. If $X$ is finite, $|X|=n$, then $S_X\cong S_n$. If a group $G$ acts on the set $X$, then (informally speaking) each element $g\in G$ implements one of those permutations of $X$, and we have a homomorphism $G\to S_X$ given by $g\mapsto[x\mapsto g\cdot x]$. The axioms from the definition of action imply that this is indeed a homomorphism.
In fact, an equivalent definition is that an action of a group $G$ on a set $X$ is simply defined as a homomorphism $\varphi:G\to S_X$. So yes, it always exists, according to the definition of group action.
In this case, $X$ is the set of the left cosets: $X=G/H$. The action of $G$ on $X=G/H$ by left multiplication is defined as $g\cdot xH=(gx)H$ for $g,x\in G$ and $xH,(gx)H\in G/H$ (left cosets). I presume the fact that this is a well-defined action was already proved earlier (in your book, if this comes from a book).

What is the significance of this part with being isomorphic to a subgroup of $S_n$?

We've already established that we have a group homomorphism $\varphi:G\to S_n$, where $S_n$ is effectively $S_X$ and this homomorphism is the action discussed above. We want to do some counting, but we have no idea how the number of elements in $G$ compares to the number of elements in $S_n$, as this homomorphism may or may not be injective or surjective or both or neither.
Isomorphism theorems are good because they tell us that certain things are precisely the same, and in particular have the same number of elements. In this case, the First Isomorphism Theorem tells us that $G/K\cong\operatorname{Im}(\varphi)$, where $\operatorname{Im}(\varphi)\le S_n$ — the image is a subgroup of the codomain group. Counting the number of elements, we see that $|G/K|=|\operatorname{Im}(\varphi)|\le|S_n|=n!$.
