Ccc and countably closed forcings are proper

Suppose first that $P$ is ccc, let $M$ be a relevant countable elementary model, and fix $p\in P\cap M$. For each dense $D\in M$, elementarity and A1 give a maximal antichain $A\in M$ with $A\subseteq D$. By F2, $A$ is externally countable. Any externally countable set $A\in M$ is a subset of $M$: elementarity supplies in $M$ a surjection from $\omega$ onto $A$, and every natural number belongs to $M$. Hence $A\subseteq D\cap M$ is predense below every condition, so $p$ itself is $(M,P)$-generic and is a master below $p$. F1 proves that $P$ is proper.

Suppose instead that $P$ is countably closed. Enumerate all dense subsets of $P$ belonging to $M$ as $⟨D_n:n<\omega ⟩$, repeating one if the family is finite. Starting with $p_0=p$, use elementarity and A1 to choose $p_{n+1}\in D_n\cap M$ with $p_{n+1}\le p_n$; every $p_n$ stays in $M$. By F3 there is $q\le p_n$ for all $n$. For every $D_n$, the condition $p_{n+1}\in D_n\cap M$ lies above $q$, so $D_n\cap M$ is predense below $q$. Thus $q$ is an $(M,P)$-master below $p$, and F1 again makes $P$ proper.

The two arguments cover the ccc and countably closed hypotheses independently and use no converse. AC is spent exactly in the maximal-antichain and enumeration/recursive-choice operations identified in steps 1.1 and 1.2. Therefore every forcing in either class is proper.