Can we choose an element from a class? Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$.
Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let
$P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$.
I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by
$$
f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\,
c_F(H_1,...,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,...,H_n$ of $H$
for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$
(the Friedrichs number is a certain numerical characteristics of a system of subspaces).
Note that all such systems of subspaces do not form a set.
Despite of this, the function $f_n$ is well-defined
(see my Question Can we take a supremum over all Hilbert spaces?).
Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that
$c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$.
Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.
I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$.
I argue as follows.
Consider arbitrary element $a\in A_{n}(c)$.
Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$
such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$.
After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that
$\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$.
Thus $a\leqslant g_n(c)$.
Since this inequality holds for every $a\in A_{n}(c)$, we conclude that
$\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.
Questions. Are all these arguments correct, say, in the axiomatic theory ZFC?
I am suspicious here because we need to choose an element (system of subspaces)
from a class (and work with this element).
Do we need here something like the Axiom of Choice?
In response to Nate Eldredge's comment: essentially, the core of my worries is the following. Unfortunately, and this is the worst, is that I do not understand if the function $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$
such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$,
is needed in the arguments above or not.
Please help me.
 A: It is often tempting to think that all our existential instantiations happen "in advance", a sort of proof theoretic "mise en place" if you will.
But they don't, and they don't have to be. For a given $a$, we pick some $H$ and $H_i$'s, and so on. At each step, we only need to instantiate finitely many quantifiers.
Now, you may still wonder, how do we choose an element from a proper class? Well, the axiom of choice has absolutely nothing to do with that. As we know, a class is really a formula, i.e. $C$ is a class when there's some $\varphi(x)$ which defines it (we allow parameters, but I'm omitting them as they are fixed through this discussion anyway). To say that $C$ is not empty is exactly to say that $\exists x\,\varphi(x)$ holds. Now apply existential instantiation and we're done.
Even if you want to choose infinitely many elements from a class, which the above reasoning doesn't allow you, we can easily prove in $\sf ZF$ that no class is finite, and so that every class must contain an infinite set: simply look at $C\cap V_\alpha$, where $V_\alpha$ is the $\alpha$th step of the von Neumann hierarchy. Since we must add new elements unboundedly often, there is some $\alpha$ such that $C\cap V_\alpha$ is infinite. If we also assume choice, then we can even argue that we surpass every possible cardinality.
