I'm studying the proof of the famous "$5B$ covering lemma":
let $\mathcal{G}$ be a family of closed balls in $\mathbb{R}^n$ satisfying: $$ \sup\{ \text{diam}(B) : B \in \mathcal{G} \} < +\infty $$ then there exists a disjoint, at most countable subfamily $\mathcal{F} \subset \mathcal{G}$ such that $$ \bigcup_{B \in \mathcal{G}} B \subset \bigcup_{B \in \mathcal{F}} 5B $$ The proof starts defining the sequence $(\mathcal{G}_i)_i$: $$ \mathcal{G}_i := \{ B \in \mathcal{G}: \frac{S}{2^{i}} < \text{diam}(B)\le \frac{S}{2^{i-1}} \} $$ where $S=\sup\{ \text{diam}(B) : B \in \mathcal{G} \}$. Now, by means of the Haussdorf's maximal principle, we extract a disjoint subfamily $\mathcal{F}_1 \subset \mathcal{G}_1$ (if $\mathcal{G}_1$ is non empty), which is maximal w.r.t inclusion. Haussdorf's maximal principle (equivalent to the axiom of choice) states that:
Given a family of sets or a family of collection of sets $\mathcal{S}$ such that every subfamily $\mathcal{S}_0$ totally ordered w.r.t inclusion has the property $\cup \{ E : E \in \mathcal{S}_0 \} \in \mathcal{S}$, then there exists an element $S^{*} \in \mathcal{S}$ which is maximal w.r.t inclusion order.
Back to the proof, we consider:
$$ \mathcal{S}= \{ \mathcal{E} \subset \mathcal{G} : \mathcal{E} \ \text{contains disjoint balls} \} $$ it is immediate to see that $\mathcal{S}$ satisfies the hypothesis of Haussdorf's maximal principle (in fact, the totally ordered subsets of $\mathcal{S}$ are those formed by "chains" of elements) , hence there is a maximal element $\mathcal{E}^{*} \in \mathcal{S}$, which contains disjoint balls by definition. We then set $\mathcal{F}_1= \mathcal{E}^{*}$.
I've got two questions in mind: is the previous application of Haussdorf's maximal principle correct (the hypothesis seems to be trivially verified, but maybe I'm missing something)? Is the principle even necessary to extract such maximal subfamily?
The use seems correct. But it seems that Zorn's lemma is a bit more appropriate. The point here is that the union over a chain of families which are pairwise disjoint is also a pairwise disjoint family. And if the chain was maximal, then the union is a maximal family.
Of course, this needs to be verified, for sake of completeness, because the existence of maximal chains need not imply the existence of maximal elements. Just look at $\Bbb N$ itself as a chain in itself. It is maximal, but there are no maximal elements.
As for the necessity, yes, some choice is necessary. It is consistent that there is a Dedekind-finite set of reals which is dense. Namely, it is a dense subset which has no countably infinite subests. Now suppose that $D$ is such set, and take $\cal G$ to be $\{B_1(x)\mid x\in D\}$. This is in fact a covering of $\Bbb R$. But any countable subfamily of $\cal G$ is finite, and cannot cover the whole line, even if scaled by a factor of $100^{100^{100}}$.