Forcing and antichains

Question

What would be a good way to show:

If $p \Vdash (\exists\alpha) \phi(\alpha)$, then there is an antichain $A$ maximal below $p$, and a set of ordinal $\{\gamma_{q} | q \in A\}$ s.t. $(\forall q \in A$) $q \Vdash \phi(\gamma_{q})$

Answer 1

Use the mixing lemma to conclude that there exists a name $\dot x$ such that $p\Vdash\dot x\in\check{\sf Ord}$ such that $p\Vdash\phi(\dot x)$.

Now consider $\{q\leq p\mid\exists\alpha\in{\sf Ord}:q\Vdash\check\alpha=\dot x\}$.

This is a dense [and open] set, so we immediately have that there is only a set of possible ordinal values for $\dot x$, and by thinning it out to a maximal antichain we have as wanted.