Suppose I have an equation in some reflexive separable Banach space $X$: $$Au=f$$ for given data $f$ and $A\colon X \to X^*$ a pseudo-monotone operator. Existence can be proved via Galerkin approximations where one takes a finite dimensional subspace $X_n \subset X$ and considers $$\langle Au_n, \varphi_j \rangle = \langle f, \varphi_j\rangle \quad\forall j=1,...,n$$ where $\{\varphi_j\}_{j=1}^n$ is a basis for $X_n$ and $u_n$ is supposed to lie in the span of this basis. Fine.
Then one derives a uniform estimate like $\lVert u_n \rVert_X \leq C$ and passes to the limit. My question is the following.
Typically there is no uniqueness of solutions for the equation, nor for the Galerkin approximations. Showing that the Galerkin approximations $u_n$ exist is done by a proof of contradiction so the proof is not constructive. This means that $u_n$ is not unique and there may be uncountable many solutions for each $n$. In this case, how can we choose a sequence and then apply Banach--Alagolu to that sequence without using the axiom of choice to select an element for each $n$?