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.
- [3]Take upper bounds for each of the sequences we've built so far.
- 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.