Finite products of standard Borel spaces are standard Borel

If $n=0$, the product is the singleton with its full two-element sigma-algebra by [F5,F6]; the unique metric on a singleton is complete and its singleton set is dense, so it is Polish and standard Borel. If a factor is empty, the product is empty and its sigma-algebra is $\{\mathrm{\varnothing }\}$; the empty metric is complete and the empty set is dense in the empty topology, so the empty space is Polish and standard Borel. These settle both boundary cases.

For any finite family of sigma-algebras, their recursive product is the sigma-algebra generated by all full measurable rectangles ${\prod }_{j<n}{A}_j$. This follows by induction from [F6]. The zero and one cases follow directly from the definitions. At the successor stage, let $\mathcal{T}$ be generated by the full $(n+1)$-rectangles. For any measurable last-coordinate set $B$, the class of $A$ in the preceding product space for which $A\times B\in \mathcal{T}$ is a sigma-algebra: it contains the whole space since the whole-space rectangle times $B$ is a full rectangle, complements subtract from that rectangle, and countable unions commute with the product by $B$. It contains every preceding full rectangle, so the inductive hypothesis gives every preceding product-measurable $A$. Thus all recursive generating rectangles belong to $\mathcal{T}$. Conversely every full rectangle is a recursive generating rectangle because its preceding rectangle is measurable. This proves equality at the successor and hence at every finite stage.

Assume $n\ge 1$ and all factors nonempty. For each $j<n$, [F1] provides a Polish presentation $h_j:E_j\to P_j$; use only finite choice [F2] to select these finitely many presentations, compatible complete metrics $d_j$, nonempty countable dense subsets $D_j$, and surjective enumerations of the $D_j$ from [F4]. The product map $h(x{)}_j=h_j(x_j)$ is a bijection from ${\prod }_{j<n}{E}_j$ onto $P={\prod }_{j<n}{P}_j$, with inverse obtained by the finitely many $h_j^{-1}$. The product is nonempty by finite choice.

Put ${\delta }_j(x,y)=\min \{1,d_j(x,y)\}$. This is a metric: symmetry and separation are inherited, and for nonnegative $a,b$, $\min (1,a+b)\le \min (1,a)+\min (1,b)$ proves the triangle inequality from that of $d_j$. Balls of radius less than $1$ are unchanged, so its topology agrees with that of $d_j$. A ${\delta }_j$-Cauchy sequence is $d_j$-Cauchy by testing every tolerance less than $1$; its $d_j$-limit is also its ${\delta }_j$-limit. Hence ${\delta }_j$ is complete. Define $D(x,y)={\sum }_{j<n}{\delta }_j(x_j,y_j)$ on $P$. Finite sums of the metric inequalities prove that $D$ is a metric.

The metric $D$ induces the product topology. For every $x$ and $\epsilon >0$, the product of coordinate ${\delta }_j$-balls of radius $\epsilon \mathrm{/}n$ lies in $B_D(x,\epsilon )$ by the finite sum inequality. Conversely, given a basic product-open neighbourhood ${\prod }_{j<n}{U}_j$ of $x$, choose positive coordinate radii $r_j$ with $B_{{\delta }_j}(x_j,r_j)\subseteq U_j$; a single positive radius smaller than every $r_j$ makes its $D$-ball lie in that rectangle. These are only finite selections. Both neighbourhood comparisons establish equality of the two topologies.

If $(x^{(k)}{)}_k$ is $D$-Cauchy, each coordinate sequence is ${\delta }_j$-Cauchy since ${\delta }_j(x_j^{(k)},x_j^{(l)})\le D(x^{(k)},x^{(l)})$. Its unique limit $x_j$ exists by step 3.1. The finite tuple $x=(x_j{)}_{j<n}$ lies in $P$. Given $\epsilon >0$, each coordinate error is eventually less than $\epsilon \mathrm{/}n$, and the maximum of the finitely many thresholds makes $D(x^{(k)},x)<\epsilon$. Thus $D$ is complete.

In each factor, the balls for ${\delta }_j$ centred in $D_j$ with positive rational radii form a countable basis. Indeed, for $x\in U$ choose $\epsilon >0$ with $B_{{\delta }_j}(x,\epsilon )\subseteq U$; choose $a\in D_j$ with ${\delta }_j(x,a)<\epsilon \mathrm{/}4$ and a rational $r$ between ${\delta }_j(x,a)$ and $\epsilon -{\delta }_j(x,a)$. Then $x\in B_{{\delta }_j}(a,r)\subseteq U$ by the triangle inequality. Centres and radii have countable enumerations, so [F4] enumerates this basis. Finite products of the basis members form a countable product basis: a tuple of their natural indices is in ${\mathbb{N}}^n$, and every basic neighbourhood contains one of these boxes. Every product-open set is therefore the union of the members of this fixed countable rectangle basis contained in it; no point-indexed selection is made.

The product of the chosen dense sets is countable: the coordinate enumerations give a surjection from ${\mathbb{N}}^n$ onto ${\prod }_{j<n}{D}_j$, and the domain is at most countable by [F4]. It is dense in $P$, because a nonempty basic rectangle meets each $D_j$, and finite choice selects a point in the product of those intersections. Hence $P$ is separable and, by the topology and completeness proved above, Polish.

Write $\mathcal{S}={⨂}_{j<n}\mathcal{B}(P_j)$. Every basic rectangle from step 5.2 belongs to $\mathcal{S}$, so every open subset of $P$ belongs to $\mathcal{S}$ as a countable union. Minimality of the Borel sigma-algebra gives $\mathcal{B}(P)\subseteq \mathcal{S}$. For the reverse inclusion, fix $j<n$ and let ${\mathcal{C}}_j=\{A\subseteq P_j:{\pi }_j^{-1}(A)\in \mathcal{B}(P)\}$. Preimages preserve complements and countable unions, so this is a sigma-algebra, and it contains every open $A$ by the projection property in [F5]. Hence it contains $\mathcal{B}(P_j)$ by [F6]. Every Borel rectangle is the finite intersection of these Borel cylinders, and is therefore Borel in $P$. Step 1.2 now gives $\mathcal{S}\subseteq \mathcal{B}(P)$, proving both inclusions.

The bijection $h$ of step 2.1 carries each full measurable rectangle in $\prod E_j$ to a full Borel rectangle in $P$, and conversely, by the exact measurable-isomorphism property of every $h_j$ in [F1]. Since images and inverse images under a bijection preserve complements and countable unions, step 1.2 identifies the transported finite product sigma-algebra with ${⨂}_{j<n}\mathcal{B}(P_j)$; step 6.2 identifies this with $\mathcal{B}(P)$. The Polish space $P$ and this bijection are thus a Polish presentation of the given product. Together with step 1.1 this proves the unchanged Statement, without AC or Countable Choice.