Does ZFC prove the universe is linearly orderable? It is consistent with ZFC that the universe is well-ordered, e.g. in $V=L$ where global choice holds. I also know that it is consistent that global choice fails (although I have no immediate example from the top of my head).
However one can try and ask a slightly weaker question, much like the axiom of choice implies every set can be linearly ordered, but the reversed implication fails; is it the same with global choice? The immediate answer is yes, it is consistent that the universe can be linearly ordered but the axiom of choice fails and therefore global choice has to fail too. But just how far can this be pushed?

Can we construct a model of ZFC in which the axiom of choice holds, but there is no linear ordering of the universe? Or does ZFC prove that the universe is linearly ordered?

One would expect that it would, because if we assume AC then the sets of ordinals already decide the universe in its entire form, and sets of ordinals can always be linearly ordered by: $$A\prec B\iff\min (A\triangle B)\in A.$$ (where $\triangle$ denotes the symmetric difference.)
 A: 
Joel nicely answers Asaf's question.
  Here I just want to add some footnotes
  to his answer.

1. Joel' argument shows that $ZFC$ cannot even prove the definable class form of axiom of choice for pairs. Historically, this was first done by with a similar argument by Easton in his 1964-thesis (printed in the Annals of Mathematical Logic).  
2. In the pre-forcing era, Mostowski had already shown that $ZFA$ + "the universe can be linearly ordered" does not imply "every set can be well-ordered" (see p.51 of Jech's book on the Axiom of Choice). 
3. As shown in the proof of Theorem 5.21 (p.71) of Jech's text, Mostwoski's argument can be transplanted to the forcing context to show that indeed $V$ can be definably linearly ordered in Cohen's so-called basic model of the failure of the axiom of choice.
A: Update. I've repaired the argument. The idea was to
use the analogue of the usual non-AC arguments, but using a class forcing instead of just Cohen reals.
Theorem. Every model of ZFC has a class forcing extension
that is a model of ZFC, in which there is no class global linear
ordering of the universe that is definable from parameters.
Proof. Let $\mathbb{P}$ be the Easton support class forcing
product $\mathbb{P}=\Pi_{\gamma\text{
reg}}\text{Add}(\gamma,\gamma\cdot 2)$, which forces to add
$\gamma\cdot 2$ many Cohen subsets to every uncountable regular
cardinal $\gamma$ (this is of course isomorphic to adding one).
Suppose that $G\subset\mathbb{P}$ is $V$-generic, and consider the
extension $V[G]$. The standard forcing arguments show that $V[G]$
is a model of ZFC, and in particular, of the axiom of choice.
Meanwhile, I claim that there is no class global linear ordering
of $V[G]$ that is definable in the language of set theory in
$V[G]$ using parameters. Suppose that there were, and that
$\psi(x,y,z)$ is a formula forced by a condition $q\in G$ to
define a linear order when used with the parameter named by $\dot
z$. Let $\gamma$ be a regular cardinal far above the support of
$q$ and any of the conditions appearing in $\dot z$. The forcing
at stage $\gamma$ added the mutually generic sets $g_\alpha$ for
$\alpha\lt\gamma+\gamma$. Let $A$ be the set of all $g_\alpha$
from the first block, that is, for $\alpha\lt\gamma$, and let $B$
be the set of $g_\beta$ from the second block, for
$\gamma\leq\beta\lt\gamma+\gamma$. Fix the corresponding canonical
names $\dot A$ and $\dot B$, as derived from $\dot G$. Suppose
without loss of generality that $A$ precedes $B$ in the definable
linear order, so that $\phi(A,B,z)$ holds in $V[G]$. Fix a
condition $p\in G$ below $q$ such that $p\Vdash\phi(\dot A,\dot
B,\dot z)$. The condition $p$ mentions less than $\gamma$ much
information about the stage $\gamma$ forcing. Thus, it details
fewer than $\gamma$ many bits of fewer than $\gamma$ many sets
each in $A$ and $B$. Furthermore, a density argument shows that
every possible initial segment of a subset of $\gamma$ occurs for
$\gamma$ many of the Cohen sets in each block. So every set in $A$
whose digits are partially specified by $p$ can be matched by a
set in $B$ that agrees with those digits, and vice versa. Since
$p$ specifies fewer than $\gamma$ many bits, there is in $V$ an
automorphism $\pi$ of the stage $\gamma$ forcing that carries out
a permutation of the coordinates, carrying altogether all the
$\alpha$s in the first block to $\beta$s in the second block and
vice versa, in such a way that happens to have $\pi(p)$ and $p$
both in $G$. We may extend $\pi$ to an automorphism of
$\mathbb{P}$, and consider the resulting transformation of names.
Since $\pi$ swaps the two blocks altogether, we have $\dot
A^\pi_G=B$ and $\dot B^\pi_G=A$. The choice of $\gamma$ ensures
that $\dot z^\pi=\dot z$. But since $p\Vdash\phi(\dot A,\dot
B,\dot z)$ we also have $\pi(p)\Vdash\phi(\dot A^\pi,\dot
B^\pi,\dot z^\pi)$, and as $\pi(p)\in G$, this means that
$\phi(B,A,z)$ in $V[G]$, which means that $B$ precedes $A$ in the
linear order, a contradiction. QED
This argument can be used to show, as Ali mentions in his answer, that there can be a definable class of pairs, having no choice function. Specifically, consider all sets of pairs, which would include the pairs of the form $\{A,B\}$ as I denote them in the proof. If we could definably select one or the other, then we fix a condition $p$ forcing which one is selected, and then find an automorphism $\pi$ that swaps the two elements of the pair, while having $\pi(p)$ still in $G$. Thus, the other set must also be selected, a contradiction. 
Corollary. Every model of set theory has a class forcing extension with a definable class of unordered pairs, such that no definable class (with parameters) selects exactly one set from each of those pairs.
