[proofplan] We prove density below $p$ by starting with an arbitrary condition $r \leq p$ and producing a stronger condition in $D_\varphi$. There are two cases: either some extension of $r$ forces $\varphi$, or no extension of $r$ forces $\varphi$. In the first case that extension already decides $\varphi$; in the second case the forcing clause for negation says that $r$ forces $\neg\varphi$. [/proofplan] [step:Take an arbitrary extension of $p$] Let $r \in \mathbb{P}$ be such that $r \leq p$. We will find $q \in \mathbb{P}$ with $q \leq r$ and $q \in D_\varphi$. [/step] [step:Use the negation clause when no stronger condition forces $\varphi$] Assume first that there is no $s \in \mathbb{P}$ such that $s \leq r$ and $s \Vdash \varphi$. By the forcing clause for negation, this is exactly the condition that $r \Vdash \neg\varphi$. Since $r \leq p$, we have $r \in D_\varphi$. Taking $q := r$, we obtain $q \leq r$ and $q \in D_\varphi$. [guided] Suppose that no stronger condition below $r$ forces $\varphi$. That is, there does not exist any $s \in \mathbb{P}$ satisfying both $s \leq r$ and $s \Vdash \varphi$. The forcing relation is defined so that negation is forced precisely by ruling out all stronger witnesses to the positive statement: a condition $r$ forces $\neg\varphi$ exactly when no extension $s \leq r$ forces $\varphi$. Therefore the present assumption gives \begin{align*} r \Vdash \neg\varphi. \end{align*} Because $r \leq p$ was already fixed, the definition of $D_\varphi$ applies to $r$: it is below $p$, and it decides $\varphi$ by forcing its negation. Hence \begin{align*} r \in D_\varphi. \end{align*} Taking $q := r$ gives the required stronger condition below $r$, since $q \leq r$ holds by reflexivity of the order on $\mathbb{P}$. [/guided] [/step] [step:Choose a stronger condition when one forces $\varphi$] It remains to consider the complementary case. Suppose there exists $s \in \mathbb{P}$ such that $s \leq r$ and $s \Vdash \varphi$. Since $r \leq p$ and $s \leq r$, transitivity of $\leq$ gives $s \leq p$. Therefore $s \in D_\varphi$. Taking $q := s$, we have $q \leq r$ and $q \in D_\varphi$. [/step] [step:Conclude density below $p$] In both cases, for the arbitrary condition $r \leq p$, we have found a condition $q \in D_\varphi$ such that $q \leq r$. Therefore $D_\varphi$ is dense below $p$. [/step]