The Stacks project

Proof. We may and do assume $c' \geq c$ and that the $\mathop{\mathrm{Ker}}(\varphi _ n)$ and $\mathop{\mathrm{Coker}}(\varphi _ n)$ are $I^{c'}$-torsion for all $n$. For $n \geq c'$ and $x \in I^{c'}E'_ n$ we can choose $y \in I^ cE_ n$ with $x = \varphi _ n(y) \bmod E'_ n[I^ c]$ as $\mathop{\mathrm{Coker}}(\varphi _ n)$ is annihilated by $I^{c'}$. Set $\psi _ n(x)$ equal to the class of $y$ in $E_ n/E_ n[I^{c'}]$. For a different choice $y' \in I^ cE_ n$ with $x = \varphi _ n(y') \bmod E'_ n[I^ c]$ the difference $y - y'$ maps to zero in $E'_ n/E'_ n[I^ c]$ and hence is annihilated by $I^{c'}$ in $I^ cE_ n$. Thus the maps $\psi _ n : I^{c'}E'_ n \to E_ n/E_ n[I^{c'}]$ are well defined. We omit the verification that $(c', \psi _ n)$ is the inverse of $(c, \varphi _ n)$ in the category. $\square$