A hypothetical decider for $A_{TM}$ yields a diagonal self-application machine

Construct a deterministic one-tape machine $D_H$ with input alphabet ${\mathrm{\Sigma }}_2$ as follows. On input a word $y\in {\mathrm{\Sigma }}_2^{\ast }$, first check whether every symbol is $1$ or $2$ and, if so, recover the unique binary word $x$ obtained by replacing $1$ by $0$ and $2$ by $1$. Use [L2] to decode $x$ as a candidate machine code. If $x$ is malformed or decodes to a machine whose input alphabet does not contain both symbols $1$ and $2$, reject. Otherwise form the coded pair $⟨x,\widehat{\bar{x}}⟩$ and run $H$ on that binary input. If $H$ accepts, then loop forever; if $H$ rejects, then accept. This machine is effective because the recoding $x\leftrightarrow \bar{x}$, the machine-code decoder, and the call to $H$ are all effective, and [L3] guarantees that the call to $H$ halts.

Let $M$ be any coded deterministic one-tape Turing machine whose input alphabet contains ${\mathrm{\Sigma }}_2$, and put $x=<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>$. On input $\bar{x}$, the preliminary checks in step 1.1 succeed, and the query sent to $H$ is exactly $⟨<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>,\widehat{\bar{x}}⟩=⟨<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>,\widehat{\overline{<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>}}⟩$. By [L1] and the correctness of the decider $H$ from [L3], $H$ accepts that query exactly when $M$ accepts $\bar{x}$. Because $D_H$ does the opposite of $H$'s answer, $D_H$ accepts $\bar{x}$ exactly when $M$ does not accept $\bar{x}$.

Step 2.1 is exactly the required diagonal property. Therefore the constructed machine $D_H$ exists.