logic - Show that a sequence of elements each realizing an isolated type over the previous realizes an isolated type

I'm trying to prove the following result which seems correct to me, but I'm not sure how to proceed. The proposition is:

Let $M$ be a structure, $A\subseteq M$, $(a_1,\dots,a_n)$ be a sequence from $M$ such that for all $i\le n$ the type $tp(a_i\,\vert\,A\cup\{a_1,\dots,a_{i-1}\})$ is isolated by $\varphi_i$, then $tp(a_1,\dots,a_n\,\vert\,A)$ is isolated by $\bigwedge_{i=1}^n\varphi_i$.

What I have so far:

Let $\Phi_i$ denote $\bigwedge_{j=1}^i\varphi_i$. By induction, in the base case $tp(a_1\,\vert\,A)$ is isolated by $\Phi_1=\varphi_1$ by hypothesis.

Now suppose that $\Phi_i$ isolates $tp(a_1,\dots,a_i\,\vert\,A)$ and $\varphi_{i+1}$ isolates $tp(a_{i+1}\,\vert\,A\cup\{a_1,\dots,a_i\})$. Let $\psi\in tp(a_1,\dots,a_{i+1}\,\vert\,A)$ and $(c_1,\dots,c_{i+1})$ from $M$ such that $M\vDash\Phi_i(c_1,\dots,c_i)\land\varphi_{i+1}(a_1,\dots,a_i,c_{i+1})$. We want to show that $M\vDash\psi(c_1,\dots,c_i,c_{i+1})$. Now since $\psi(a_1,\dots,a_i,x)\in tp(a_{i+1}\,\vert\,A\cup\{a_1,\dots,a_i\})$, we have $M\vDash\psi(a_1,\dots,a_i,c_{i+1})$.

Now because $M\vDash\Phi_i(c_1,\dots,c_i)$ I know that $tp(c_1,\dots,c_i\,\vert\,A)=tp(a_1,\dots,a_i\,\vert\,A)$, but it seems that I need to show that the two tuples realize the same type over $A\cup\{c_{i+1}\}$ in order to conclude. I'd appreciate any hint to how to proceed from here, or a counterexample if the result is not correct.

Answer

There's an issue with the statement of the proposition you're trying to prove: The formula $\varphi_i$ is a formula over $A\cup\{a_1,\dots,a_{i-1}\}$, not over $A$, so it can't appear as a conjunct in a formula purporting to isolate $\text{tp}(a_1,\dots,a_n/A)$.

It is true that if $\text{tp}(a_i/A\cup\{a_1,\dots,a_{i-1}\})$ is isolated for all $i$, then $\text{tp}(a_1,\dots,a_n/A)$ is isolated, and an inductive argument of the type you wrote down will work. I would recommend trying first trying to prove this, and then extracting the formula that works from the proof.