§ Axiom of Choice and Zorn's Lemma

I have not seen this "style" of proof before of AoC/Zorn's lemma by thinking of partial functions (A→B)(A \rightarrow B) as monotone functions on (A∪⊥→B)(A \cup \bot \rightarrow B).

§ Zorn's Lemma implies Axiom of Choice

If we are given Zorn's lemma and the set AiA_i, to build a choice function, we consider the collection of functions (f:∏iAi→→Ai∪⊥)(f: \prod_i A_i \rightarrow \rightarrow A_i \cup \bot) such that either f(Ai)=⊥f(A_i) = \bot or f(Ai)∈Aif(A_i) \in A_i. This can be endowed with a partial order / join semilattice structure using the "flat" lattice, where ⊥<x\bot < x for all xx, and ⊥⊔x=x\bot \sqcup x = x. For every chain of functions, we have a least upper bound, since a chain of functions is basically a collection of functions fif_i where each function fi+1f_{i+1} is "more defined" than fif_i. Hence we can always get a maximal element FF, which has a value defined at each F(Ai)F(A_i). Otherwise, if we have F(Ai)=⊥F(A_i) = \bot, the element is not maximal, since it is dominated by a larger function which is defined at AiA_i. Hence, we've constructed a choice function by applying Zorn's Lemma. Thus, Zorn's Lemma implies Axiom of Choice.