Derivation of g-formula

I am looking over a paper that derives the g-formula. The setting is the following: two treatments $$A_0, A_1$$ and a sole covariate $$Z$$

The assumptions are:

• Counterfactual consistency: $$E[Y|A_0=a_0,A_1=a_1]=E[Y^{a_0,a_1}|A_0=a_0,A_1=a_1]$$
• Sequential conditional exchangeability: $$E[Y^{a_0,a_1}|A_0,A_1,Z]=E[Y^{a_0,a_1}|A_0,Z]$$ and $$E[Y^{a_0,a_1}|A_0]=E[Y^{a_0,a_1}]$$
• Positivity: $$0< P(A_1=1| Z=z_1,A_0=a_0)<1$$ and $$0

The derivation states: \begin{align*} E(Y^{a_0,a_1} ) &= E{E(Y^{a_0,a_1} | A_0)}\\ &= E{E(Y^{a_0,a_1}| A_0 = a_0)}\\ &=E[E{E(Y^{a_0,a_1}|A_0 =a_0,Z,A_1)|A_0 =a_0}]\\ &=E[E{E(Y^{a_0,a_1} |A_0 =a_0,Z,A_1 =a_1)|A_0 =a_0}]\\ &=E[E{E(Y |A_0 =a_0,Z,A_1 =a_1)|A_0 =a_0}]\\ &=\sum_{z_i}E(Y |A_0 =a_0,Z =z_1,A_1 =a_1)P(Z =z_1 |A_0 =a_0) \end{align*}

I do not understand why we can go from $$E{E(Y^{a_0,a_1} | A_0)}$$ to $$E{E(Y^{a_0,a_1}| A_0 = a_0)}$$ (same with the fourth). Is it because of the seq. conditional exchangeability assumption? If so, why?

Starting with the quantity of interest, notice that $$E[Y^{a_1,a_0}] = E[Y^{a_1,a_0} | A_0=a_0]$$ given the exchangeability assumption that $$E[Y^{a_1,a_0}] = E[Y^{a_1,a_0} | A_0]$$ (which requires the corresponding positivity assumption). In the paper, the authors first step is iterative expectation by $$A_0$$. Then given the exchangeability assumption, we can freely condition on any particular value for $$A_0$$ (i.e., $$A_0 = a_0$$). Either approach here works. The approach I used above directly uses exchangeability (and doesn't require the iterative expectation), whereas the referenced paper uses two steps to get to this result. However, we end up at the same place.
Now we can apply iterative expectation by $$Z_1$$ to get $$E[Y^{a_1,a_0} | A_0=a_0] = E[E\{Y^{a_1,a_0} | Z_1, A_0=a_0 \} | A_0=a_0]$$ Now, with the other exchangeability assumption (with positivity), we can arrive at $$E[E\{Y^{a_1,a_0} | Z_1, A_0=a_0 \} | A_0=a_0] = E[E\{Y^{a_1,a_0} | Z_1, A_0=a_0, A_1 = a_1 \} | A_0=a_0]$$ Again, I use the exchangeability assumption directly for this quantity, whereas the authors of the paper first use iterative expectation and then exchangeability to condition on a particular value of $$A_1$$.
Then by causal consistency $$E[E\{Y^{a_1,a_0} | Z_1, A_0=a_0, A_1 = a_1 \} | A_0=a_0] = E[E\{Y | Z_1, A_0=a_0, A_1 = a_1 \} | A_0=a_0]$$ Here, we need $$a_1,a_0$$ for the causal consistency step, hence why we condition on those values throughout. The final step in the paper only works when $$Z_1$$ is discrete, so this result is more general.