Prikry forcing is kappa-plus-cc but not ccc

There are at most $\kappa$ finite stems. To see this without hiding cardinal arithmetic, use F4 to fix a bijection $b:\kappa \times \kappa \to \kappa$, recursively code a nonempty finite sequence by repeated application of $b$, and tag the code with its length. This injects all finite sequences from $\kappa$ into $\omega \times \kappa$, whose cardinality is $\kappa$ by F4 because $0<\omega \le \kappa$. The ambient dependency The Axiom of Choice is not used in this count: one existing bijection is fixed and the recursion is finite.

Given ${\kappa }^{+}$ conditions, if all their stems were distinct, step 1.1 would inject ${\kappa }^{+}$ into $\kappa$, contrary to F5. Two therefore have the same stem, and F1 makes them compatible. Thus no antichain has cardinality ${\kappa }^{+}$; under ZFC, any antichain of cardinality at least ${\kappa }^{+}$ contains a ${\kappa }^{+}$-sized subfamily. By F3, ${\mathbb{P}}_U$ is ${\kappa }^{+}$-cc.

For every $\alpha <\kappa$, the tail $A_{\alpha }=\kappa \setminus (\alpha +1)$ lies in $U$: it is the intersection of the fewer than $\kappa$ complements of the singleton points at most $\alpha$. Hence $p_{\alpha }=(⟨\alpha ⟩,A_{\alpha })$ is a condition. If $\alpha \mathrm{\ne }\beta$, a common extension would have a stem end-extending both distinct one-entry stems, which is impossible. Thus $\{p_{\alpha }:\alpha <\kappa \}$ is an antichain of size $\kappa$. Since $\kappa$ is uncountable, F3 shows that the forcing is not ccc.