The paper "An Axiomatic Approach to Forcing in a General Setting" by R. Freire and P Holy includes the proof of Lemma 4.2.
(Note that in the paper a 'generic filter' means a filter in a partial order P and C is a class of sets and $F_G()$ is a valuation under G and other items are in the notes under the question).
My question is : what is the reasoning behind the last step ?
Lemma 4.2. Let D $\in$ C be such that D is dense in P. If G is a generic filter, then G intersects D.
Proof.
Let G be a generic filter and assume for a contradiction that G $\cap$ D = $\emptyset$.
Making use of axioms (*) and (**), it follows that
$$M[G] \models \neg \exists x \; x \in F_G (\check{D}) \cap F_G(\dot{G}) $$
By axiom (4 – the Truth Lemma), we may thus find p $\in$ G such that
$$p \Vdash \neg \exists x \; x \in \check{D} \cap \dot{G} $$
By Lemma 4.1, equivalently
$$\forall q \leq p \; \neg [q \Vdash \exists x \; x \in \check{D} \cap \dot{G}] $$
Since D is dense, we may fix q $\leq$ p in D.
Last step:
But then
$$ q \Vdash \check{q} \in \check{D} \cap \dot{G}$$
so contradicting the above.
So the question is : what is the reasoning behind "But then $ q \Vdash \check{q} \in \check{D} \cap \dot{G}$"
i.e. why should G contain the q $\leq$ p that is in D ?
Notes :
(*) Names for ground model objects
$ \forall a \in M \; \exists \check{a} \in M \; \forall G \; F_G(\check{a}) = a $
(**) Name for generic filters
$\exists \dot{G} \in C \; \forall G \; F_G(\dot{G})=G$
Lemma 4.1 : $ p \Vdash \neg \varphi \iff \forall q \leq p \; \neg [q \Vdash \varphi]$
Best Answer
The reason is axiom (5) Definability Lemma. For every $q$, it is true that $q$ forces that $G$ contains $q$ (which is the interpretation of $\check q\in\dot G$).