$\require{AMScd}$ I am studying the proof that the ordering principle does not imply the axiom of choice in Jech's book "The Axiom of Choice" (Section 5.5). Let $P$ be the set of finite partial functions $\omega\times\omega\longrightarrow 2$ and let $B$ be its completion. We consider the symmetric extension $\mathcal N$ obtained from a countable transitive model $M$ of ZFC (+ $V=L$ if you wish) determined by the group all permutations of $\omega$ in $M$ and the finite support filter.
For each finite set $e\subset \omega$, Jech defines a map $u\mapsto u:e$ on $B$ whose algebraic meaning is clear: taking $\bar e = \omega\setminus e$, we have $P\cong P_e\times P_{\bar e}$, where $P_e$ is the set of finite partial functions $e\times\omega\longrightarrow 2$ given by $p\mapsto (p:e,p:\bar e)$, where $p:e = p\cap (e\times\omega\times 2)$, and we have a commutative diagram $$ \begin{CD} B@>>> B_e\times B_{\bar e}\\ @AAA @AAA\\ P@>>> P_e\times P_{\bar e} \end{CD} $$ where $B_e$ y $B_{\bar e}$ are the completions of $P_e$ and $P_{\bar e}$, respectively. Then, the first row isomorphism is denoted by $u\mapsto (u:e,u:\bar e)$, and so the map $u\mapsto u:e$ is the unique complete homomorfism $B\longrightarrow B_e$ extending the restriction map $p\mapsto p:e$ defined on $P$.
However, I have no insight at all about the meaning of $u\mapsto u:e$ with regard to forcing. For instance, in the proof of Lemma 5.23, Jech reduces the proof of equation (5.33) to prove (under suitable hypotheses):
$$ p\cdot (\|\underline v\in \underline x\|: e) = p\cdot (\|\underline v\in \pi\underline x\|:e).\hspace{2cm}(*) $$
My question is: do $\|\phi\|:e$ have any "natural" meaning making equations like this "plausible"? or in other words: Why an equation like $(*)$ should be expected to be true (when the context is known, of course)? Can such equations be translated in a standard way in terms of $\Vdash$?
In fact, Jech says:
Since $\|\underline v\in \underline x\|:e\in B_e$, it suffices to show: For every $q\leq p$ such that support$(q\setminus p)\subseteq e$,
\begin{array}{lrl} (5.36)&(i)& \mbox{if }q\Vdash \underline v\in \underline x, \mbox{ then } (\exists r\leq q)r\Vdash \underline v\in \pi\underline x,\\ &(ii)&\mbox{if }q\Vdash \underline v\notin \underline x, \mbox{ then }(\exists r\leq q)r\Vdash \underline v\notin \pi\underline x. \end{array}
But I cannot see the connection between (5.36) and equation $(*)$ from the algebraic definition of $u\mapsto u:e$. In fact, this is the only step of the whole Section 5.5 that I have not been able to fill myself.
Is there any reason or procedure by which one sees $(*)$ and comes to say "in practice, this means (5.36)"?
Of course, I am interested in this concrete case, but my question is more general than that. For instance, at a previous step, Jech reduces (5.26) to (5.27). In this case I have had no trouble in proving that (5.27) implies (5.26), but still I have the same question: How does one realizes that, in practice, (5.26) means (5.27)? How shoud an equation like (5.27) be thought?
AMScd
for drawing diagrams, rather than "by hand arrays". $\endgroup$