Below is the proof of Proposition 2.1.4 from Ethier and Kurtz' Markov Processes. I need help understanding a line in the proof below.
A process $X$ is $\{\mathcal{F}_t\}-$progressive if for each $t\ge 0$ the restriction of $X$ to $[0,t]\times \Omega$ is $\mathcal{B}[0,t]\times \mathcal{F}_t-$measurable. Let $\tau$ be $\{\mathcal{F}_t\}-$stopping time. Define $X^\tau$ and $Y$ by $X^\tau (t)=X(\tau \wedge t)$ and $Y(t)=X(\tau+t)$, and define $\mathcal{G}_t=\mathcal{F}_{\tau \wedge t}$ and $\mathcal{H}_t=\mathcal{F}_{\tau+t}, t\ge 0$. Then we have:
(e) $\mathcal{G_t}$ is a filtration and $X^\tau$ is both $\mathcal{G}_t$ progressive and $\mathcal{F}_t$ progressive.
(f) $\mathcal{H}_t$ is a filtration and $Y$ is $\mathcal{H}_t$ progressive.
Proof of (f): We've already shown that $\mathcal{H}_t$ is a filtration. Fix $t\ge 0$. By part (e) the mapping $(s,\omega)\to X((\tau(\omega)+t)\wedge s,\omega)$ from $([0,\infty]\times \Omega, \mathcal{B}[0,\infty]\times \mathcal{F}_{\tau+t})$ into $(E,\mathcal{B}(E))$ is measurable, as is the mapping $(u,\omega)\to (\tau(\omega)+u,\omega)$ from $([0,t]\times \Omega,\mathcal{B}[0,t]\times \mathcal{F}_{\tau+t})$ into $([0,\infty]\times \Omega, \mathcal{B}[0,\infty]\times \mathcal{F}_{\tau+t})$. The mapping $(u,\omega)\to X(\tau(w)+u,\omega)$ from $([0,t]\times \Omega, \mathcal{B}[0,t]\times \mathcal{F}_{\tau+t})$ into $(E,\mathcal{B}(E))$ is a composition of the first two mappings so it too is measurable. Since $\mathcal{H}_t=\mathcal{F}_{\tau+t}$, $Y$ is $\mathcal{H}_t$ progressive.
I don't understand the bold part of this proof. From progressive measurability, we need to fix $t\ge 0$, but here we have the domain of the time set $[0,\infty]$. So how do we use progressive measurability here? Also, (e) gives us $\mathcal{F}_{\tau \wedge t}$-progressive, so I don't understand how we get $([0,\infty]\times \Omega, \mathcal{B}[0,\infty]\times \mathcal{F}_{\tau+t})$ measurable.
By (e),
$$[0,T] \times \Omega \ni (s,\omega) \mapsto X(\varrho \wedge s)(\omega)$$
is $B[0,T] \otimes \mathcal{F}_{\varrho \wedge T}$-measurable for any $T>0$ and any $(\mathcal{F}_t)_{t \geq 0}$-stopping time $\varrho$. As $\varrho \wedge T \leq \varrho$ implies $\mathcal{F}_{\varrho \wedge T} \subseteq \mathcal{F}_{\varrho}$, see 2.1.4(c), we find that the mapping is $\mathcal{B}[0,T] \otimes \mathcal{F}_{\varrho}$-measurable. Applying this for the stopping time $\varrho := \tau+t$ (with $t$ fixed), we obtain that
$$[0,T] \times \Omega \ni (s,\omega) \mapsto X((\tau+t) \wedge s)(\omega) \tag{1}$$
is $B[0,T] \otimes \mathcal{F}_{\tau+t}$-measurable. Since
$$\begin{align*} &\{(s,\omega] \in [0,\infty] \times \Omega; X((\tau+t) \wedge s)(\omega) \in B\} \\ &= (\{\infty\} \times \underbrace{\{\omega; X(t+\tau)(\omega) \in B\})}_{\in \mathcal{F}_{\tau+t} \, \, \text{by 2.1.4(d)}} \cup \bigcup_{n \geq 1} \underbrace{\{(s,\omega) \in [0,N] \times \Omega; X((\tau+t) \wedge s)(\omega)\}}_{\in \mathcal{B}[0,\infty] \otimes \mathcal{F}_{\tau+t} \, \, \text{by (1)}} \\ &\in \mathcal{B}[0,\infty] \otimes \mathcal{F}_{\tau+t} \end{align*}$$
for any measurable set $B \in \mathcal{B}(E)$, we conclude that
$$[0,\infty] \times \Omega \ni (s,\omega) \mapsto X((\tau+t) \wedge s)(\omega) $$
is $B[0,\infty] \otimes \mathcal{F}_{\tau+t}$-measurable.