[proofplan] We prove totality by showing that, for each coordinate $m$, the set of Hechler conditions with stem length greater than $m$ is dense. Since the generic filter meets every ground-model dense set, the union of the compatible stems has a value at every coordinate. To prove domination, we fix a ground-model function $g$ and strengthen an arbitrary condition by replacing its bounding function with a pointwise upper bound for both the old bound and $g$. Every later stem extension must then put all coordinates beyond the original stem above this strengthened bound, so the generic real eventually dominates $g$. [/proofplan]

[step:Show that stems in the generic filter are compatible] Let $p = (s,h)$ and $q = (t,k)$ be conditions in $G$. Here $s,t \in \mathbb{N}^{<\mathbb{N}}$ are finite stems and $h,k: \mathbb{N} \to \mathbb{N}$ are bounding functions. Since $G$ is a filter, there is a condition $r = (u,\ell) \in G$ such that $r \leq p$ and $r \leq q$. By the definition of the Hechler order, $u$ extends both $s$ and $t$. Hence $s$ and $t$ agree on their common domain. Therefore the union \begin{align*} d_G := \bigcup\{s : \exists h: \mathbb{N} \to \mathbb{N} \text{ with } (s,h) \in G\} \end{align*} is a well-defined partial function from $\mathbb{N}$ to $\mathbb{N}$. [/step]

[step:Meet dense sets of conditions with long stems]For each $m \in \mathbb{N}$, define \begin{align*} D_m := \{(s,h) \in \mathbb{D} : \operatorname{lh}(s) > m\}. \end{align*} We use the standard convention that a finite sequence $s$ of length $L = \operatorname{lh}(s)$ has domain $\{0,1,\dots,L-1\}$, so the coordinate $m$ is defined exactly when $\operatorname{lh}(s) > m$. We claim that $D_m$ is dense in $\mathbb{D}$. Let $(s,h) \in \mathbb{D}$. If $\operatorname{lh}(s) > m$, then $(s,h) \in D_m$. If $\operatorname{lh}(s) \leq m$, define $t \in \mathbb{N}^{<\mathbb{N}}$ by requiring that $t$ extends $s$, $\operatorname{lh}(t) = m+1$, and \begin{align*} t(n) := h(n) \end{align*} for every $n$ with $\operatorname{lh}(s) \leq n \leq m$. Then $(t,h) \leq (s,h)$, because $t$ extends $s$, the bounding function is unchanged, and every newly added stem value satisfies $t(n) = h(n) \geq h(n)$. Also $(t,h) \in D_m$. Thus $D_m$ is dense. Since $D_m \in V$ and $G$ is $V$-generic, $G \cap D_m \neq \varnothing$. Therefore, for every $m \in \mathbb{N}$, some stem appearing in $G$ has length greater than $m$. Since the stems in $G$ are compatible, $d_G(m)$ is defined for every $m \in \mathbb{N}$. Hence $d_G: \mathbb{N} \to \mathbb{N}$ is total.[/step]

[guided]Fix a coordinate $m \in \mathbb{N}$. To prove that $d_G(m)$ is defined, we need to force the generic filter to contain some condition whose finite stem includes coordinate $m$. Under the standard convention, a stem of length $L$ has domain $\{0,1,\dots,L-1\}$, so coordinate $m$ is included exactly when $L > m$. This is why we introduce the set \begin{align*} D_m := \{(s,h) \in \mathbb{D} : \operatorname{lh}(s) > m\}. \end{align*} The set $D_m$ belongs to the ground model $V$, because it is defined from the forcing notion $\mathbb{D}$ and the integer $m$. We verify that it is dense. Let $(s,h) \in \mathbb{D}$ be arbitrary. If the stem $s$ already has length greater than $m$, then $(s,h)$ itself lies in $D_m$. Suppose instead that $\operatorname{lh}(s) \leq m$. We extend the stem to length $m+1$, because length $m+1$ is the first length that guarantees coordinate $m$ is in the domain. Define $t \in \mathbb{N}^{<\mathbb{N}}$ so that $t$ agrees with $s$ on the domain of $s$, has length $m+1$, and assigns \begin{align*} t(n) := h(n) \end{align*} for each newly added coordinate $n$ with $\operatorname{lh}(s) \leq n \leq m$. These are exactly the coordinates added when passing from domain $\{0,1,\dots,\operatorname{lh}(s)-1\}$ to domain $\{0,1,\dots,m\}$. Then $t$ extends $s$. The condition $(t,h)$ keeps the same bounding function, so the inequality between bounding functions required by the order is automatic. For every new coordinate, the Hechler order requires $t(n) \geq h(n)$, and this holds because $t(n) = h(n)$. Therefore $(t,h) \leq (s,h)$, and $\operatorname{lh}(t) = m+1 > m$, so $(t,h) \in D_m$. Thus every condition has a stronger condition in $D_m$, meaning $D_m$ is dense. By definition, $G$ is $V$-generic precisely means that $G$ meets every [dense subset](/page/Dense%20Subset) of $\mathbb{D}$ that belongs to $V$. Therefore $G \cap D_m \neq \varnothing$. Hence some condition in $G$ has a stem whose domain contains coordinate $m$. Because the stems in $G$ are mutually compatible, all such stems give the same value at coordinate $m$. Since $m$ was arbitrary, $d_G$ is a total function $\mathbb{N} \to \mathbb{N}$.[/guided]

[step:Strengthen an arbitrary condition to impose eventual domination of a fixed ground-model function] Fix $g \in V \cap \mathbb{N}^{\mathbb{N}}$. Let $p = (s,h) \in \mathbb{D}$ be arbitrary. Define $k: \mathbb{N} \to \mathbb{N}$ by \begin{align*} k(n) := \max\{h(n), g(n)\}. \end{align*} Then $k \in V \cap \mathbb{N}^{\mathbb{N}}$, and $(s,k) \leq (s,h)$ because the stem is unchanged and $k(n) \geq h(n)$ for every $n \in \mathbb{N}$. Let $N := \operatorname{lh}(s)$. We claim that $(s,k)$ forces $g(n) \leq d_G(n)$ for every $n \geq N$. Indeed, let $q = (t,\ell) \leq (s,k)$ and let $n \geq N$ with $n < \operatorname{lh}(t)$. Since $\operatorname{lh}(s) \leq n < \operatorname{lh}(t)$, the coordinate $n$ is one of the coordinates added beyond the stem $s$, and the corrected Hechler order gives $t(n) \geq k(n) \geq g(n)$. Thus any condition extending $(s,k)$ whose stem decides $d_G(n)$ decides it to be at least $g(n)$. For each $n \geq N$, the dense-set argument from the previous step gives arbitrarily strong extensions with stem length greater than $n$. Hence $(s,k)$ forces $d_G(n)$ to be defined and $g(n) \leq d_G(n)$ for every $n \geq N$. [/step]

[step:Conclude that the generic real dominates every ground-model function] For functions $a,b: \mathbb{N} \to \mathbb{N}$, write $a \leq^* b$ to mean that there exists $N \in \mathbb{N}$ such that $a(n) \leq b(n)$ for every $n \geq N$. Define \begin{align*} E_g := \{(s,k) \in \mathbb{D} : (s,k) \text{ forces } g(n) \leq d_G(n) \text{ for every } n \geq \operatorname{lh}(s)\}. \end{align*} Here $(s,k)$ forces a statement means that every $V$-generic filter containing $(s,k)$ satisfies that statement under the usual interpretation of the $\mathbb{D}$-name $d_G$. The set $E_g$ belongs to $V$, because $g$, $\mathbb{D}$, and the forcing relation for $\mathbb{D}$ are in $V$. The previous step shows that for every condition $(s,h) \in \mathbb{D}$ there is a stronger condition $(s,k) \in E_g$. Hence $E_g$ is dense in $\mathbb{D}$. Since $G$ is $V$-generic, $G \cap E_g \neq \varnothing$. Choose $(s,k) \in G \cap E_g$ and set $N := \operatorname{lh}(s)$. By the defining property of $E_g$ and the [truth lemma for forcing](/theorems/6518), the interpretation of the generic real satisfies \begin{align*} g(n) \leq d_G(n) \end{align*} for every $n \geq N$. Hence $g \leq^* d_G$. Since $g \in V \cap \mathbb{N}^{\mathbb{N}}$ was arbitrary, $d_G$ dominates every ground-model function from $\mathbb{N}$ to $\mathbb{N}$. [/step]