I have added a conjunction with !q2 since we want to derive the transition relation for the states where !q2 holds. Note that phi&!q2=phi[q2<-0]&!q2 holds, where phi[q2<-0] denotes the formula phi where all occurrences of q2 are replaced with 0.

For the same reason, (q0 <-> a | a & Xq0) & !a is equivalent to (q0 <-> 0 | 0 & Xq0) & !a which is again equivalent to (q0 <-> 0) & !a.