I am trying to prove that the mapping $(t,\omega) \mapsto \big(\min(\tau(\omega),t),\omega\big)$ is measurable from $\mathcal{B}([0,t]) \otimes \mathcal{F_t} \to \mathcal{B}([0,t]) \otimes \mathcal{F_t} $
Where $\tau$ is a stopping time i.e $\tau:\Omega \to \mathbb{R_+} \cup \{\infty\}$ s.th $\{\tau \leq t\} \in \mathcal{F_t}$
Now if we take $A \in \mathcal{F_t} \implies \{\tau \leq t\}$ which implies $\big(\min(\tau(\omega),t),\omega\big) \iff \big(\tau(\omega),\omega\big) $
So now we have to prove that $(t,\omega) \mapsto \big(\tau(\omega),\omega\big)$ is measurable from $\mathcal{B}([0,t]) \otimes \mathcal{F_t} \to \mathcal{B}([0,t]) \otimes \mathcal{F_t} $
Now if we choose an $A\in \mathcal{B}([0,t]) \otimes \mathcal{F_t} $, where $A_1 \in \mathcal{F_t}$ and $A_2 \in \mathcal{B}([0,t])$,
then on taking the inverse image we get $\big(\tau(\omega),\omega\big)^{-1}(A)=\big(\tau(\omega),\omega\big)^{-1}(A_2 \times A_1)$ and as $\omega$ does not change on taking the inverse image , and $\tau(\omega) \leq t \implies \big(\tau(\omega),\omega\big)^{-1}(A) \in \mathcal{B}([0,t]) \otimes \mathcal{F_t} $
I am not so sure about the proof because at the last step I make an implicit assumption that if $\tau(\omega) \in \mathcal{B}([0,t])$ then so does $t$ which makes sense intuitively but I can't write it down rigorously. I would be grateful if you could help me out. Thanks
In order to prove the measurability of the mapping
$$([0,t] \times \Omega, \mathcal{B}[0,t] \times \mathcal{F}_t) \ni (s,\omega) \mapsto f(s,\omega) := (\min(\tau(\omega),s),\omega) \in ([0,t] \times \Omega, \mathcal{B}[0,t] \times \mathcal{F}_t) $$
recall that the intervals $[0,s]$, $0 \leq s \leq t$, are a generator of the Borel $\sigma$-algebra $\mathcal{B}[0,t]$ and that it therefore suffices to show
$$f^{-1}([0,s] \times F) \in \mathcal{B}[0,t] \otimes \mathcal{F}_t$$
for any $s \geq 0$ and $F \in \mathcal{F}_t$. To this end, we note that by definition of $f$
$$\begin{align*} f^{-1}([0,s] \times F) &= \{(r,\omega) \in [0,t] \times \Omega; \omega \in F, \min(r,\tau(\omega)) \leq s\} \\ &= \{(r,\omega) \in [0,t] \times \Omega; \omega \in F, \min(r,\tau(\omega)) \leq s, \tau(\omega) \leq s \}\\ &\quad \cup \{(r,\omega) \in [0,t] \times \Omega; \omega \in F, \min(r,\tau(\omega)) \leq s,\tau(\omega>s\} \\ &= \big( [0,t] \times (F \cap [\tau \leq s]) \big) \cup \big( [0,s] \times (F \cap [\tau>s]) \big). \end{align*}$$