Rigorous proof of the Jordan-Hölder Theorem As far as I am aware, the standard books on abstract algebra (Lang, Dummit, Rotman, Grillet, etc.) do not give a rigorous proof of the Jordan-Hölder Theorem. Here are two examples from Lang and Grillet:




As you can see, there's a lot of prose in these proofs. I do not have any issues with these "prose-laden" proofs per se; however, I do like to replace them with their formal counterparts whenever possible. To some of you this may seem rather trivial, but to me it isn't: I genuinely do not understand these sorts of proofs of the Jordan-Hölder Theorem. Let me explain why.
Let $G$ be a group (finite or otherwise) with identity $e$. To say that two normal series $(H_i)_{0\leq i\leq n}$, $(K_j)_{0\leq j\leq m}$ of $G$ are equivalent means that

*

*$n=m$, and

*$(\forall i)(i\in[0,n-1]\Rightarrow \frac{H_i}{H_{i+1}}\,\simeq\,\frac{K_{\phi(i)}}{K_{\phi(i)+1}})$,

where $\phi:[0,n-1]\rightarrow[0,n-1]$ is a permutation of the interval $[0,n-1]$. Now go back to the proofs of Lang and Grillet: Is it at all obvious how these proofs satisfy (1) and (2)? (They don't even bother to construct a candidate for $\phi$.)
Logically speaking, I should be able to give a formal proof of (1) and (2) being satisfied for two composition series, no?
Ok—Let $(H_i)_{0\leq i\leq n}$, $(K_j)_{0\leq j\leq m}$ be two composition series of $G$. By Schreier, we know that these two series have equivalent refinements: $(H'_i)_{0\leq i\leq n'}$, $(K'_j)_{0\leq j\leq n'}$. This means that we have a permutation
$$\psi:[0,n'-1]\rightarrow [0,n'-1]$$
such that
$$(\forall i)(i\in[0,n'-1]\Rightarrow \frac{H'_i}{H'_{i+1}}\,\simeq\,\frac{K'_{\psi(i)}}{K'_{\psi(i)+1}}).$$ Now I have to show that (1) and (2) hold for our original series. That partly means I should have to prove (either by construction or by contradiction) that their exists a permutation of the interval $[0,n-1]$ for which (2) holds: this means that I should be able to assume $i\in[0,n-1]$ and show that the consequent must also hold. Let us fix some notation:
\begin{align*}
\mathcal{A}&=\{X\ |\ (\exists i)(i\in[0,n'-1]\ \land\ X=H'_i/H'_{i+1})\}\\
\mathcal{B}&=\{X\in\mathcal{A}\ |\ K\simeq\{e\}\}\\
\mathcal{C}&=\{X\ |\ (\exists i)(i\in[0,n-1]\ \land\ X=H_i/H_{i+1})\}
\end{align*}
Then $\mathcal{A}-\mathcal{B}=\mathcal{C}$. Let $\mathcal{A'},\mathcal{B'},\mathcal{C'}$ denote the same sets except with $K'_{\psi(i)}/K'_{\psi(i)+1}$, $K_i/K_{i+1}$ and $m$ replacing $H'_i/H'_{i+1}$, $H_i/H_{i+1}$ and $n$. Then also $\mathcal{A'}-\mathcal{B'}=\mathcal{C'}$. You can say that this shows that the non-trivial factors of each refinement are the factors of its original series. This is roughly what Grillet says mid-paragraph.
But why should $m=n$? I should be able to derive a contradiction by supposing $n\ne m$, no? Moreover, how does this prove the existence of a permutation $\phi$ satisfying the formula $$(*)\ \ \ (\forall i)(i\in[0,n-1]\Rightarrow \frac{H_i}{H_{i+1}}\,\simeq\,\frac{K_{\phi(i)}}{K_{\phi(i)+1}})?$$ The part of the proof involving the permutation is essentially ignored by both Lang and Grillet. Is it because it is unimportant? Then why include it in the definition of equivalence?
In any case, I would appreciate any help I can get w.r.t the proof of the implication $(*)$.
EDIT:
Two votes have been cast to close this question; I am not sure why. I will restate my request in order to once again establish that I have asked this question in good faith. What I am looking for is very simple:
(a) a proof that deduces $H_i/H_{i+1}\simeq K_{\phi(i)}/K_{\phi(i)+1}$ from the premise $i\in[0,n'-1]$ (essentially a demonstration of a logical implication). I would appreciate it if you could try to only invoke Schreier as an existential result (i.e. not putting further assumptions on the form of the equivalent refinements);
(b) a proof that shows (and not merely says) why $m=n$. This has to be a formal set theoretic proof of equinumerosity.
Please do not give me a prose proof. I already have Lang et al. for that. Also, I have eyes and I can read. Therefore, please, do not give me chewed up versions of Lang's proof.
I think this is a reasonable demand. If you think that I have violated the rules, please leave a comment explaining why. Thank you.
EDIT 2:
Consider the following lists:
\begin{align*}
&0,1,\ldots,n-1 &(a)\\
&H_0/H_1,\ldots, H_{n-1}/H_n &(b)\\
&H'_0/H'_1,\ldots, H'_{n'-1}/H'_{n'} &(c)\\
&K'_{0}/K'_{1},\ldots, K'_{n'-1}/K'_{n'} &(d)\\
&K_0/K_1,\ldots, K_{m-1}/K_m &(e)\\
&0,1,\ldots,m-1 &(f)
\end{align*}
Using the notation employed above, I will try to explain my difficulty with the proof 3.0 (maybe the next patch giving us version 4.0 will be the lucky one?), submitted below, in its author's favourite medium for doing mathematics: prose.
The strategy is very simple: if you can show that you can put list $(a)$ and list $(f)$ in one to one correspondence by only using the lists $(b)-(e)$, then you can be said to have shown that $m=n$. The lists $(a)$ and $(b)$ are in a one to one correspondence through the rule $i\mapsto H_i/H_{i+1}$. Moreover, $(b)$ and its surrogate list in $(c)$ are also bijectively connected, e.g. by the map which sends each $H_i$ to the $H'_j$ such that $H_i=H'_j$ where $j$ is the maximal of the set of all such indices (you can probably do this in some other way too); denote it by $r_i$. One can connect the lists $(f)$, $(e)$ and $(d)$ in a similar manner.
That leaves us with $(c)$ and $(d)$. I don't see how these two lists can be connected other than by using the identifications sanctioned by $\psi$. For example: I will send $H_i/H_{i+1}$ to $H'_{r_i}/H'_{r_{i}+1}$ which is itself sent to $K'_{\psi(r_i)}/K'_{\psi(r_i)+1}$ etc. Hence, if we can put surrogates of $(b)$ in $(c)$ and those of $(e)$ in $(d)$ in one-to-one correspondence, we are done.—But.—As the author of the submitted answer has already admitted, it is possible, by using $\psi$, to take two different elements of list $(a)$ to the same element of list $(d)$. Well then, better say goodbye to our bijection showing $m=n$.
That $\psi$ only allows nontrivial to nontrivial is irrelevant to this particular issue: because it can do so—wait for it—trivially, e.g. by allowing us to send every nontrivial element of $(c)$ to one particular nontrivial element of $(d)$ (since one can identify different members of a series with each other). Incidentally, this shows why the "identifications" don't give us a very robust method of counting in this case. The question is whether the correspondence between the surrogates of the elements of $(b)$ in $(c)$ and those of the elements of $(e)$ in $(d)$ is, according to $\psi$, unique.
In the absence of uniqueness of the partial correspondence between $(c)$ and $(d)$, how else can one use $\psi$ to connect $(b)$ and $(e)$? Merely asserting "just use $\psi$!" won't do; you have to specify the manner in which one has to use $\psi$ exactly.
This sums up the lack clarity present in Lang's proof and the post below. This is what I wanted cleared up with a standard set theoretic proof. We seem to have so many testimonies, but, strangely, very little actual evidence. I am sure that such a bijection exists (cumbersome or not), though a little more honesty would perhaps make us admit that it is not near at hand.
Quite simply, the method  suggested  is inadequate.
A last word: I do not approve of recycling the constructions involved in Schreier. You can invoke Schreier as an existential theorem. That should be enough.
 A: Both invoke Schreier's Theorem (Lang implicitly). Lang's statement of Schreier's Theorem is:

Theorem 3.4. (Schreier) Let $G$ be a group. Two normal towers of subgroups ending with the trivial group have equivalent refinements.

Rewritten.
(This seems like a bit of a wasted exercise; the whole below is contained in Lang)
The proof of Schreier’s Theorem is explicit in Lang, invoking the Butterfly Lemma:

Butterfly Lemma (Zassenhaus): Let $A$ sand $C$ be subgroups of a group $G$, and let $B\triangleleft A$ and $D\triangleleft C$ be subgroups. Then
  $$\frac{(A\cap C)B}{(A\cap D)B} \cong \frac{(A\cap C)D}{(B\cap C)D}.$$

If you simply in-line the proof of Schreier’s Theorem into the proof of Jordan-Holder (which is, let me say, a dumb thing to do; that’s the whole point of invoking theorems already proven), you get:
Suppose that
$$1=H_n\triangleleft H_{n-1}\triangleleft\cdots\triangleleft H_1 \triangleleft H_0 = G$$
and
$$1 = K_m \triangleleft K_{m-1}\triangleleft\cdots \triangleleft K_1 \triangleleft K_0=G$$
are two composition series for $G$. For each $i$, $0\leq i\leq n$, $j$, $0\leq j\leq m$, define
$$\begin{align*}
H_{ij} &= (H_i\cap K_j)H_{i+1}\\
K_{ji} &= (H_i\cap K_j)K_{j+1}.
\end{align*}$$
It is now straightforward to verify that $\{H_{ij}\}$ is a refinement of $\{H_i\}$,, with $H_{i+1}=H_{im}$, $H_i=H_{i0}$, and the terms $H_{i1},\ldots,H_{i,m-1}$ interpolating between them; and that $\{K_{ji}\}$ is similarly a refinement of $\{K_j\}$. From the Butterfly Lemma, we have
$$\frac{H_{ij}}{H_{i,j+1}} \cong \frac{K_{ji}}{K_{j,i+1}}$$
so the  bijection from $[0,n]\times[0,m]$ to $[0,m]\times[0,n]$ sending $(i,j)$ to $(j,i)$ establishes the equivalence of the two subnormal series (making this a bijection from $[0,nm+n+m]$ to itself showing the bijection would require formulas that only obscure the fact that you have a bijection; this is better than trying to construct such a bijection).
This is explicit in Lang. The Butterfly Lemma is proven, and Schreier’s Theorem is proven as above.
Now, because the original series are composition series, we know any refinement is obtained by repeating terms. So for each $i$ there exists a unique $j_i$ such that $H_{ij_i}\neq H_{i,j_i+1}$, with $H_{i,j_i+1}=\cdots = H_{im}=H_{i+1}$ and $H_{ij_i}=\cdots = H_{i0}=H_i$; thus, $\frac{H_{ij_i}}{H_{i,j_i+1}}= \frac{H_i}{H_{i+1}}$. 
Symmetrically, for each $j$ there exists a unique $i_j$ such that $K_{ji_j}\neq K_{j,i_j+1}$, with the quotient being the same as $\frac{K_j}{K_{j+1}}$. 
All other quotients in either refinement are trivial. Thus, there are exactly $n$ nontrivial quotients associated with the subnormal series $\{H_{ij}\}$ (one for each $i$); and there are exactly $m$ nontrivial quotients associated with the subnormal series $\{K_{ji}\}$ (one for each $j$). The bijection $\psi$ associates nontrivial quotients with nontrivial quotients, and trivial quotients with trivial quotients, so the bijectivity of $\psi$ demonstrates that $n=m$: the number of nontrivial quotients in each of the refinement series is the same, because the two refinement series are known to be equivalent. As this is the number of terms in the two original composition series, the two original composition series have the same length.
The whole of the above could be easily summarized by using multisets (sets that include multiplicity). It leads to less cumbersome notational issues, but the information conveyed is exactly the same. 
Now define $\phi\colon [0,n]\to[0,m]$ (which is the same as $[0,n]$ because $m=n$) by $\phi(i)=j_i$. Then
$$\frac{H_i}{H_{i+1}} = \frac{H_{i,j_i}}{H_{i,j_i+1}}\cong \frac{K_{j_i,i}}{K_{j_i,i+1}}.$$
But $\frac{K_{j_i,i}}{K_{j_i,i+1}}$ is nontrivial, hence we must have $i=i_{j_i}$ (by uniqueness of $i_k$ for each $k$). That is
$$\frac{H_i}{H_{i+1}} = \frac{H_{i,j_i}}{H_{i,j_i+1}}\cong \frac{K_{j_i,i}}{K_{j_i,i+1}} = \frac{K_{j_i,i_{j_i}}}{K_{j_i,i_{j_i}+1}} = \frac{K_{j_i}}{K_{j_i+1}}.$$
This proves the two composition series are equivalent. 
This is not done explicitly in Lang because (i) it is cumbersome, (ii) a lot of it is contained in Schreier’s Theorem which has already been proven; and (iii) it should be obvious if you have understood both what Schreier’s Theorem says, and what a refinement does to a composition series: you are simply inserting a bunch of trivial factors to both series and then defining an explicit bijection, but a bijection that is easiest to express with index pairs rather than simple indices. Trying to translate that into a bijection of simple indices would involve bijections $[0,n]\times[0,m]\to[0,nm+m+n]$ which would only serve to obscure what is going on by adding layers of notation. For most people, that is undesirable. Because the bijection identifies the composition factors that “matter”, you know that a bijection exists between the composition factors of the original two series, even if writing it down explicitly is way too cumbersome. The existence of the bijection is not being “ignored” in the proof: the bijection is known to exist because it has already been proven to exist. There’s a difference between “I don’t see where the bijection is given” and “they don’t give the bijection.”  All of the above was also contained in the previous version of this post.

Your question about $i\neq j$ with $\frac{H_i}{H_{i+1}}\cong \frac{H_j}{H_{j+1}}$ is not a challenge to the proof; there is no “contradiction” because you are not understanding what the theorem says and does no say. The theorem does not say two composition factors of a group cannot be isomorphic. It says that the list of composition factors is unique up to permutation, but the list accounts for multiplicity. 
For example, take $G=C_{12}$, the cyclic group of order $12$, generated by $x$. Here are three different composition series for $G$:
$$\begin{align*}
1 \triangleleft \langle x^6\rangle \triangleleft \langle x^3\rangle \triangleleft C_{12}\quad &(1)\\
1 \triangleleft \langle x^6\rangle \triangleleft 
\langle x^2\rangle\triangleleft C_{12} \quad&(2)\\
1\triangleleft \langle x^4\rangle \triangleleft \langle x^2\rangle \triangleleft C_{12} \quad&(3)
\end{align*}$$
Call the terms of the first series $H$s, the second $Ks$, and the third $M$s.
Given a composition series $1=H_m\triangleleft H_{m-1}\triangleleft \cdots \triangleleft H_{1}\triangleleft H_0=G$, define the (ordered) list of composition factors associated with this series to be the tuple $(\frac{H_0}{H_1},\frac{H_1}{H_2},\ldots,\frac{H_{m-1}}{H_m})$. 
The list of composition factors for the first series is $(C_3,C_2,C_2)$; the list for the second series is $(C_2,C_3,C_2)$; the list for the third series is $(C_2,C_2,C_3)$. Between the $H$s and the $K$s, you want a map $\psi\colon \{0,1,2\}\to\{0,1,2\}$ such that $H_i/H_{i+1} \cong K_{\psi(i)}/K_{\psi(i)+1}$: you could take $\psi(0)=1$, $\psi(1)=0$, and $\psi(2)=2$. 
Now you say: take $i$ (say, $i=0$). Now let $k$ be the largest index such that $K_k/K_{k+1}$ is isomorphic to $H_0/H_1$; that would be $K_2$, since $H_0/H_1\cong C_2$, and $K_2/K_3\cong C_2$. Let $j$ be the largest index such that $H_j/H_{j+1}\cong K_2/K_3$: that would be $j=1$, since $H_1/H_2\cong C_2$. Now $1\neq 0$; you ask “where is the contradiction?” The answer is: nowhere. There is no contradiction because what you are doing is not negating the conclusion of Jordan-Holder; it does not assert that there are no repetitions in the list of composition factors, only that however many repetititons you find in one composition series will be exactly the same in all composition series. Just as above: every composition series for $C_{12}$ will include one factor isomorphic to $C_3$, and two factors isomorphic to $C_2$.
All of this is contained in Lang’s proof. All it takes is to read the previous invoked theorems and do a bit of thinking. The proof there is neither “comical” (a joke), nor is it “not rigorous”. It may not satisfy you, but that is not the standard by which rigor is measured in the world. 
