What is the first order formulation of Zorn's lemma in the language of set theory? Very often in notes of courses in set theory you find the assertion that in ZF the Axiom of choice (AC) is equivalent to Zorn's Lemma (ZL) (which is equivalent to Well Ordering Principle which it equivalent to Cardinality Tricotomy etc). Some proof of the statement might follow, or at least of the easy part, namely $\text{ZL}\rightarrow\text{AC}$. And still, regardless of having mentioned that the equivalence is a theorem of ZF, little is said about the syntax behind the statement and the proof. I'm finding it difficult finding even the formulation of Zorn's lemma in the language of set theory $\mathcal{L}=\{\in\}$. 
The formulation of AC would be the following. Let's assume that we are familiar with the formulas "$f$ is a functions whose domain is $A$" and "$y$ is the image of $x$ by $f$" (namely $f(x)=y$), AC can be written as
$$
\forall A \exists f ((f \text{ is a formula whose domain is } A)\wedge \forall x (x\in A \rightarrow \exists y (f(x)=y \wedge y\in x))).
$$

My question would be what is the formulation of Zorn's Lemma in the language of set theory.

Since this question deals with my incapability of finding a pertinent standard source, the mentioning of any such source is welcomed. 
Bonus question Consider a language $\mathcal{L}=\{\leq\}$ with a binary relation and the theory $T$ of partial orders in said language. Consider a formulation of ZL given by the following second order formula $\phi$:
$$
(\forall X (X \text{ is a chain } \rightarrow \exists c \forall x (x\in X\rightarrow x\leq c))\rightarrow \exists m\, (m \text{ is a maximal element)}.
$$
If $\phi$ a theorem of $T$?
 A: This is probably going to be very unilluminating, but here goes:

"If, in a partial order $P$, every chain $C$ has an upper bound, then $P$ has a maximal element."

Let's start with the obvious bit: how do we talk about partial orders in set theory? Note that we could also ask, "How do we talk about groups in set theory?" or rings, or fields, or . . . and the answers will be basically the same.
Definition 1. A partial order is an ordered pair $(P, L)$, where 


*

*$P$ is a set,

*$L$ is a binary relation on $P$, and

*$L$ satisfies the axioms of a partial order: transitivity, reflexivity (I'm viewing $L$ as $\le$, not $<$, here), antisymmetry.
This might seem non-set-theory-ish, but remember: we have ordered pairs and powersets! This means that all the above can be formalized in set theory with little difficulty:
Definition 2 (all ZF). A partial order is a set $x$ such that


*

*$x=\{a, \{a, b\}\}$ for some sets $a, b$ (this is the Kuratowski ordered pair); and these $a, b$ satisfy

*$b\subseteq a^2$ (note that "$a^2$", the set of Kuratowski ordered pairs of elements of $a$, can be constructed via repeated powerset and separation),

*$\forall x, y, z\in a, [(x, y), (y, z)\in b\implies (x, z)\in b]$ (this is transitivity - for simplicity I've written "$(\cdot, \cdot)$" instead of the full Kuratowski ordered pair),

*$\forall x\in a, [(x, x)\in b]$ (reflexivity), and

*$\forall x, y\in a[(x, y)\in b\wedge (y, x)\in b\implies x=y]$ (antisymmetry).
So this lets us talk about partial orders. 
Similarly, if $(a, b)$ is a partial order, then a chain is a set $x\subseteq a$ such that $\forall y, z\in x[(y, z)\in b\vee (z, y)\in b]$. And maximal elements and upper bounds of chains are similarly straightforwardly definable.
All of this, when spelled out formally, yields a perfectly normal first order sentence. Birds-eye view, it has the form $$\forall x[P(x)\wedge\forall zQ(x,z)\implies \exists w M(x,w)]$$ where $P$, $Q$, and $M$ are abbreviations for the formulas defining "is a partial order," "is either not a chain in -, or which is a chain in - and has an upper bound," and "is a maximal element in -" respectively. Written out entirely, it's quite long; if you really want to you can easily write it out for yourself, but I'd think for a while first about exactly what it is you're hoping to see.

As to your bonus question: sorry to disappoint, but second-order logic is terrible. 
There is no nice proof system for second-order logic (at least, not with the standard semantics - with Henkin semantics there is, but then with Henkin semantics it's just first-order logic in disguise). This can be made precise and proved in a variety of ways. Just to get started, note that set-theoretic questions can get folded in. For instance, the $\varphi$ you mention is a second-order consequence of the definition of partial order iff the axiom of choice is true! Another good example is that we can write an explicit second-order sentence which is a tautology iff the continuum hypothesis holds. 
So in order for us to answer your question, you need to tell us what set-theoretic assumptions you're making - in particular, whether you assume AC; and I believe at that point the answer won't really be interesting. :)
I believe I've written more about the general terribleness of second-order logic elsewhere, for instance,  in my answer to Complete and correct deductive axiom for SOL
