The intermediate model theorem:
If $M\subseteq N\subseteq M[G]$ are all models of $\sf ZFC$, with $G$ generic over $M$, then $N$ is a generic extension of $M$, and $M[G]$ is a generic extension of $N$.
The proofs I've seen (Jech lemma 15.43 and in Grigorieff's "Intermediate submodels and generic extensions in set theory") are somewhat roundabout, as they pass through complete boolean algebras. Is there a more "direct" proof using just posets?
Furthermore, given some poset $P$, a generic $G$ and $M\subseteq N\subseteq M[G]$, the theorem gives me some $Q\in M$ and $Q$-generic filter $H$ such that $N=M[H]$. I want to understand $Q$ in terms of $P$. What can I say about it? Can I construct it more or less explicitly?