Why is Kan's $Ex^\infty$ functor useful? I've always heard that Kan's $Ex^\infty$ functor has important theoretical applications, but the only one I know is to show that the Kan-Quillen model structure is right proper. What else is it useful for?
I'm looking for something more than the existence of a functorial fibrant replacement functor for the Kan-Quillen model structure, for which one can simply appeal to the small object argument.
As far as I know, the nice properties of the monad $Ex^\infty: sSet \to sSet$  are summed up in the following list (all model-categorical terms are with respect to the Kan-Quillen model structure on $sSet$):


*

*$Ex^\infty$ preserves finite products.

*In fact, $Ex^\infty$ preserves finite limits and filtered colimits.

*$Ex^\infty$ preserves fibrations and acyclic fibrations.

*$Ex^\infty$ preserves and reflects weak equivalences.

*$X \to Ex^\infty X$ is an anodyne extension for every $X$.

*$Ex^\infty X$ is fibrant for every $X$.

*(Have I missed something?)
Thus, $Ex^\infty$ is a functorial fibrant replacement for the Kan-Quillen model structure which preserves finite limits, fibrations, and filtered colimits. The above list is rather redundant. For instance, I've listed (1) separately from (2) because I'm thinking of it as a "monoidal" property rather than an "exactness" property.
Some consequences are that:


*

*The Kan-Quillen model structure is right proper.

*The weak equivalences of the Kan-Quillen model structure are stable under filtered colimits.

*The simplicial approximation theorem follows easily if you happen to independently know that $sSet$ is Quillen equivalent to $Top$.

*What else?
For instance, I think I have the impression that (1) implies something important about simplicial categories, but I'm not sure what.
The applications I've listed can all be proven in different ways, and might even be inputs to proving the above properties of $Ex^\infty$. Ideally I'd like something meatier.
 A: The Ex^∞ functor provides a powerful criterion for detecting weak equivalences
of simplicial sets.
The specific construction of Ex^∞ is crucial for such a criterion.
Specifically, the simplicial Whitehead theorem states
that simplicial homotopy equivalences of Kan complexes
are simplicial maps that have a relative-homotopy-lifting property
with respect to the inclusions ∂Δ^n→Δ^n.
Using Kan's Ex^∞ functor we can extend this criterion to detect
weak equivalences of arbitrary simplicial sets.
More precisely, since ∂Δ^n and Δ^n are compact objects,
any map ∂Δ^n→Ex^∞(X) or Δ^n→Ex^∞(X) factors through some Ex^m(X),
which allows us to use the adjunction between Sd^m and Ex^m
to show that weak equivalences between arbitrary simplicial sets
are precisely those simplicial maps that have a relative-homotopy-lifting property
with respect to iterated subdivisions of ∂Δ^n→Δ^n,
with an additional caveat that we may increase the number of subdivisions
and the homotopy itself can be subdivided.
A: Another application of Kan's $\def\Ex{{\rm Ex}} \Ex^∞$ functor
is that it allows one to write down completely explicit
functorial factorizations of arbitrary simplicial maps.
Acyclic cofibration followed by a fibration:
$$X→\Ex^∞ X⨯_{\Ex^∞ Y}(\Ex^∞ Y)^{Δ^1}⨯_{\Ex^∞ Y}Y→Y.$$
Cofibration followed by an acyclic fibration:
$$X→\Ex^∞((Δ^1⨯X) ⊔_X Y)⨯_{\Ex^∞ Y}(\Ex^∞ Y)^{Δ^1}⨯_{\Ex^∞ Y}Y→Y.$$
The traditional approach to constructing model structures may create
an impression that such factorizations are somehow inexplicit and/or purely theoretical.
The above formulas dispel such impressions.
A: Another thing for which Kan Ex$^{\infty}$ functor is useful is actually in the construction of the Kan-Quillen model structure. It morally gives a purely algebraic version of the simplicial approximation theorem (the version involving subdivision) which allows you to avoid the use of topological spaces in the proof.
This is very apparent in Cisinski's proof of the existence of the Kan-Quillen model structure from his book "Les préfaisceaux comme modèles des types d'homotopies". 
In his approach it follows quite formally, from the theory of test categories and what we now call the theory of Cisinski model structures, that there is a model structure on simplicial sets, where the cofibrations are the monomorphisms and the weak equivalences are the realization weak equivalences. But it is unclear what the fibrations are.
With a bit of work one can see that the fibrant objects are the Kan complexes and the fibrations between fibrant objects are the Kan fibrations, but it is considerably harder to show that in general the fibrations are the the Kan fibrations.
This is at this point that Cisinki introduces Kan's Ex$^{\infty}$ and uses its good property to show this last fact (if I remember correctly, he essentially shows that any Kan fibration is a retract of the pullback of its image by Kan Ex$^{\infty}$, which is a Kan fibration between Kan complexes, hence an actual fibration).
A sign that this last result is hard, is that in very similar situations, like the Joyal model structure, or Lurie's model structure on Marked simplicial sets, but where one does not have an analogue of Kan Ex$^{\infty}$, this last results (that one can characterize fibrations between general objects by our naive lifting property) does not hold.
A similar, but more direct approach to give a purely combinatorial construction of the Kan Quillen model structure, also relying on Kan's Ex$^{\infty}$ functor, but which uses more explicit constructions instead of the theory of test categories and Cisinski model structures, has been given by S.Moss.
Note that the most classical proof of the existence of the Kan-Quillen model structure uses topological spaces and the simplicial approximation theorem, which in the end relies on a machinery very similar to that of Kan's $Ex^{\infty}$. Though another type of purely combinatorial proof (but very non-constructive) of the existence of the Kan-Quillen model structure uses the theory of minimal fibrations instead. (see for example Joyal & Tierney notes on simplicial homotopy theory, and as pointed by Denis Nardin, this is also Quillen's original proof).
In a recent preprint I've shown that S.Moss argument can actually be made into a fully constructive proof of the existence of the Kan-Quillen model structure. Two different (also constructive) proofs of this fact of this results have been also given since by Gambino,Sattler and Szumilo. One of their proof also relies on Kan's Ex$^{\infty}$, but use a more 'topologically minded' argument and involve less work on the combinatorics of Ex$^{\infty}$ than S.Moss argument, the other proof use yet a different set of ideas coming from homotopy type theory (It is based on a direct proof of the equivalence extension property, so in spirit it is close to the proofs involving minimal fibrations, but bypass the use of minimal fibration).
