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?

actuallychoosing uniformly. Think of each $H$ as a room: you first enter the room, then you have a lot of rooms for the choice of subspaces, so you enter into one of the rooms. You compute something and you get a real number. You keep that real number, and you now use Replacement to instantly do the same for all rooms and all the rooms inside of those rooms.You are not choosing anything.$\endgroup$logically equivalentto the $\exists F\forall x\varphi(x,F(x))$ (here $F$ is a 2nd order object), and while that is true that the two are equivalent in $\sf ZF+GC$, this is not a rule of logic, nor we use this in the proof. So there's no need to choosefor all Hilbert spacessuch system of closed subspaces. So we are not doing that. $\endgroup$8more comments