Two settings for a proof of Zorn's lemma implies the Axiom of Choice

$ \newcommand{\emt}{\varnothing} \newcommand{\chain}{\mathcal{C}} \newcommand{\imply}{\Rightarrow} \newcommand{\dom}{\operatorname{dom}} $ The question is going to be a lot verbose. But would you help? First, I would like to express AC and ZL in formal first-order language.

AC) $\forall X: [\emt \notin X \imply \exists c \in X \to \cup X: \forall A \in X: c(A) \in A]$

ZL) $\forall C \in \chain(S, \le):\exists x \in S:\forall y \in C:y \le x \imply \exists x \in S:\forall x \in S: \neg y< x$

Notation)
$X \to Y$ is the set of all functions from $X$ to $Y$.
$\chain(S, \le)$ is the set of all chains in $(S, \le)$.
$f|_A$ is the restriction of $f$ to $A$

When I first tried to prove AC from ZL, I used a setting in which $E$ and its order $\le$ is defined: (This is the proof given in a textbook)

$$ \begin{aligned} E &= \{(A,c) ~|~ A \subseteq X,~ c \in A \to \cup A,~ \forall B \in A: c(B) \in B\}\\ \le &= \{((A_1,c_1),(A_2,c_2)) \in E\times E ~|~ A_1 \subseteq A_2,~ c_2|_{A_1} = c_1 \} \end{aligned} $$

$E$ is the set of the pairs of choice function $c$ and its domain $A$. Then, ZL is applied to the poset $(E,\le)$.

(You can skip this.) To apply ZL to $(E, \le)$, for each $C \in \chain(E,\le)$, I defined the domain ($C$ is a chain) $$ B = \bigcup_{(A,c) \in C}A = \{D \in X~|~\exists(A,c) \in C: D \in A \} $$ and the corresponding choice function $$ c'\in B \to \cup B,~\forall D \in B:\forall (A,c) \in \chain:[D \in A \imply c'(D) = c(D)] $$ Then, $c'$ is well-defined and $(B,c')$ is an upper bound of $C$. Now we can apply ZL and this gives a maximal $(M,c_M)$ in which $M$ must be equal to $X$.

So I tried to be familiar with the setting. But when I started to learn real analysis by Folland (1999), in Theorem 0.7, I saw another setting for ZL.

To show that $|X| \le |Y| \lor |Y| \le |X|$ for all sets $X$ and $Y$, the author defined the set $$ I = \{f \subseteq X \times Y~|~f \text{ is an injection}\} $$ and formed a poset ordered by inclusion, $(I, \subseteq)$. This is different from the setting for ZL implies AC in that the domain of the function $f$ (denoted by $A$ in the above proof) is not explicitly paired as an element of the poset; thus, set inclusion $\subseteq$ can be used to form a poset without need for a new partial order definition in contrast to the former setting. However, because the domain is not specified, to find the domain of each element of $I$, I had to define $$ \dom f = \{x \in X ~|~ \exists y \in Y: (x,y) \in f\} $$

Now, I guess that, with $\dom f$, this setting seems not quite logically different from the former setting. But this looks a lot simpler. If I adopt this setting to show ZL implies AC, I may define

$$ J = \{c \subseteq X \times \cup X~|~ c \text{ is a function},~\forall A \in \dom c: c(A) \in A\} $$

and form $(J, \subseteq)$. Now, let's summarize.

Question) Is this a matter of choice to use $(E,\le) $ or $(J, \subseteq)$?

Note that if $(A,c)\in E$, then $A=\operatorname{dom}(c)$. Note that if $f,g$ are two functions and $f\subseteq g$, then $g\restriction\operatorname{dom}(f)=f$.

So really $J$ and $E$ are "practically the same".