Countable saturation of an ultraproduct over omega

An ultraproduct over a nonprincipal ultrafilter on $\omega$ realizes each countable finitely satisfiable type. For the first $n$ formulas, their coordinate simultaneous-witness set $E_n$ belongs to the ultrafilter by the Łoś theorem. Replace it by $E_n\cap [n,\infty )$ and choose at coordinate $i$ a witness to as many initial formulas as that coordinate permits. This finite number tends to infinity modulo the ultrafilter, so the resulting product class realizes every formula. More generally countably incomplete ultrafilters admit the same descending-set diagonalization. This statement does not assert saturation at every larger cardinal.