Recall that a trivial Kan fibration is a morphism in sSet that has the right lifting property with respect to the boundary inclusions ∂Δn ↪ Δn for all n ≥ 0. The following is well-known:
Proposition. A morphism in sSet has the left lifting property with respect to all trivial Kan fibrations if and only if it is a monomorphism.
The standard proof uses the fact that monomorphisms in sSet admit a cellular decomposition, and the fact that the class of morphisms that have the left lifting property with respect to another class is closed under transfinite composition, pushouts, and retracts.
Yet, the proposition is equivalent to the axiom of choice! Indeed, let ∇ : Set → sSet be the right adjoint of the functor X ↦ X0. (∇ is also known as cosk0.) It is clear that, if f : X → Y is a surjection, then ∇f : ∇X → ∇Y is a trivial Kan fibration: indeed, f : X → Y is a surjection if and only if ∇f : ∇X → ∇Y has the right lifting property with respect to ∂Δ0 ↪ Δ0, and for any map f : X → Y, ∇f : ∇X → ∇Y has the unique right lifting property with respect to ∂Δn ↪ Δn for all n ≥ 1. But 0 → ∇Y is a monomorphism, so if the proposition holds, then ∇f : ∇X → ∇Y must have a section; and ∇ : Set → sSet is fully faithful, so f : X → Y has a section if and only if ∇f : ∇X → ∇Y has a section.
A few minutes thinking should reveal where we use the axiom of choice in the proof of the proposition. While it is true that every monomorphism in sSet is a relative cell complex (provided you allow arbitrarily many cells to be attached at each stage), it would appear that we need the axiom of choice to deduce that every relative cell complex is in the class of morphisms generated by the boundary inclusions under transfinite compositions and pushouts: after all, we have to choose the order in which we attach the cells!
But that is not the end of the story: if that were the only problem, then we could deduce that trivial Kan fibrations have the right lifting property with respect to monomorphisms in sSet whose codomain is well-orderable. This is not obviously true either – in fact, it seems that we need the axiom of choice to show that the class of morphisms with the left lifting property with respect to another class is closed under coproducts and transfinite composition!
So perhaps the moral of the story is that the theory of cofibrantly-generated model categories is non-constructive in subtle, easily missed ways.