Trivial forcing recovers the ground model

A nonempty filter in the singleton preorder must be $\{1\}$. Every dense subset contains 1, since 1's only extension is itself. Hence G meets every ground dense subset and is the unique M-generic. Here G=P belongs to M.

For any ground name tau, its valuation recursion using G can be carried out inside M since G is a set in M and M satisfies ZF. It agrees with the external recursion: every subname and its sole possible coefficient are in M, and induction on name rank identifies the predecessor values and their set image at each step. Thus ${\tau }_G\in M$. This gives $M[G]\subseteq M$, while F2 gives $M\subseteq M[G]$. Consequently $M[G]=M$.

F1 says that truth at the valuations is equivalent to a member of G forcing the formula. Its only member is 1, and the extension is exactly M by step 2.1. These substitutions prove the first display; F2 then replaces check-name values by the original parameters. For example empty and singleton names have values $\mathrm{\varnothing }$ and $\{\mathrm{\varnothing }\}$, so 1 forces $\check{\mathrm{\varnothing }}\in \check{\{\mathrm{\varnothing }\}}$ and does not force their equality. No Choice is used.