What kind of Choice am I making in this argument? I have an argument that's supposed to imply Choice, but I'm afraid it may be using some choice. If it does, how much choice?
This is the part of the argument that might use some Choice. I marked the parts that I think MIGHT use Choice ("[1]", "[2]", "[3]").
Assume:


*

*$X$ is compact. (Every open cover (collection of open sets whose union is $X$) has a finite subcover.)

*We are given a collection of open sets $P$ from $X$ such that:

*

*$P$ covers $X$.

*For every totally ordered subcollection of $P$, there is an element in $P$ which contains the union of that subcollection (i.e. every chain has an upper bound, the hypothesis of Zorn's Lemma).



Claim:


*

*$P$ has a maximal element (the conclusion of Zorn's Lemma).


Proof?:


*

*Let $P_0 := P$.

*Assume $P$ has no maximal element.

*At step 0:

*

*[1]Take a finite subcover of $P_0$.

*Since it's finite, we can select the open sets to be independent: each open set contains a point not in the others.

*Call it $Q_0$.

*For each element $q_i$ in $Q_0$, set $s_{i, 0} := q_i$.

*Set $P_1$ to be the elements of $P$ which are greater (strictly contain) some element of $Q_0$.

*

*None of the elements of $Q_0$ were maximal, so $P_1$ covers $X$.



*At step $n$:

*

*Do the same process as above to construct $P_{n+1}$.

*[2]Choose $s_{i, n+1}$ to be some element of $Q_n$ (as in the base case) which contains $s_{i, n}$.


*For limit step $<\alpha$:

*

*[3]Take upper bounds for each of the sequences we've built so far.

*

*The sequences we built form totally ordered subcollections of $P$, so each has an upper bound in $P$.


*Since each element of the original cover $Q_0$ is contained in the upper bound, this forms a finite subcover.

*Adjoin these upper bounds to the sequences.

*As before: Choose $P_{\alpha}$ to be the elements of $P$ which are greater than these upper bounds.


*Since we always remove the finite subcover from the next step, each sequence is a sequence of distinct elements (though not necessarily distinct from each other).

*By transfinite induction, we inject the ordinals into $P$.

*By contradiction, $P$ has a maximal element.

 A: All three points you suspect choice are using choice. Although in the third one you can perhaps remove it.

*

*There might be many finite subcovers at each step, and you have to choose one each time. How do you choose it?


*There might be many candidates at each time. How do you choose them? Ideally, you have a finite enumeration of $Q_n$, and you choose from it. But how do you choose the enumeration of $Q_n$? Choice hides right there.
The same use of the axiom of choice essentially comes into play when you create $Q_0$. In order to do this, you need to enumerate the finite subcover and go over the enumeration, but different enumerations give different $Q_0$'s, so you need the axiom of choice once you do this infinitely many times.


*If you mean one upper bound for each sequence, you might have to resort to the axiom of choice; if you take all of them, then it's probably fine.
Upon re-reading, I think this trick is not applicable here.
In either case, in the general case, I see absolutely no way of removing the need for the axiom of choice here. I'm not even sure that you can bound the amount of choice needed for the first issue, let alone for the third. In the second issue you only need to be able and choose finite numerations, that's not "that bad", but it's still something.
