Can we choose a sequence of Hilbert spaces?

Question

Let $n$ be a fixed natural number. Let $H$ be a complex Hilbert space and $H_1,\dotsc,H_n$ be closed subspaces of $H$. Set $H_0\mathrel{:=}H_1\cap H_2\cap\dotsb\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,\dotsc,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\lVert P_n\dotsm P_2 P_1-P_0\rVert \mathrel| c_F(H_1,\dotsc,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,\dotsc,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,\dotsc,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristic of a system of subspaces).

As explained in a previous question, there is no problem with the definition of the supremum.

The question is about the following argument, which seemingly requires the axiom of choice for proper classes.

By the definition of the supremum for every natural number $m\geqslant 1$ there exist a Hilbert space $H^{(m)}$ and a system of its closed subspaces $H^{(m)}_1,...,H^{(m)}_n$ such that $c_F(H^{(m)}_1,...,H^{(m)}_n)\leqslant c$ and $\|P^{(m)}_n...P^{(m)}_2 P^{(m)}_1-P^{(m)}_0\|>f_n(c)-1/m$. Now we can use these systems of subspaces, for example, we can form the orthogonal direct sum $\bigoplus_{m=1}^\infty H^{(m)}$.

Question: are these innocent arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because I need to choose infinite number of systems of subspaces simultaneously. If I understand things correctly, we need to use here the Axiom of Choice. But all systems of subspaces $(H;H_1,...,H_n)$ with $c_F(H_1,...,H_n)\leqslant c$ do not form a set and the Axiom of Choice works with sets! So we need to use here something like the "Axiom of Choice for classes", but I do not know such an Axiom. Therefore I think that the arguments above are not correct, but they are so innocent...

Help me please understand if the arguments are correct or not correct. In other words, can we choose a sequence of systems of subspaces of Hilbert spaces as above or we cannot do this?

Answer 1

For every $m\ge1$ we have a proper class $A_m$ of tuples $(H,H_1,…,H_n)$ satisfying the described condition.

Now invoke Scott's trick and construct a subset $A'_m⊂A_m$ for each $m\ge1$, consisting of tuples with the minimal rank in $A_m$. (This part of the construction does not use the axiom of choice.)

Since $A'_m$ are ordinary sets, we can apply the ordinary axiom of choice to extract a specific tuple for each $m\ge1$.

As a side remark, Scott's trick is also used in various constructions with classes, such as quotients of classes, and, more generally, colimits of classes. See the nLab article category of classes for more information.