"Cayley's theorem" for Lie algebras?

Groups can be defined abstractly as sets with a binary operation satisfying certain identities, or concretely as a collection of permutations of a set. Cayley's theorem ensures that these two definitions are equivalent: any abstract group acts as a collection of permutations of its underlying set, and this action is faithful.

Similarly, rings can be defined abstractly as sets with a pair of binary operations satisfying certain identities, or concretely as a collection of endomorphisms of an abelian group. There is a "Cayley's theorem" here as well: any abstract ring acts as a collection of endomorphisms of its underlying abelian group, and this action is faithful.

The situation for Lie algebras seems much less clear to me. The adjoint representation is not generally faithful, and Ado's theorem comes with qualifications and doesn't have the simplicity of the two theorems above. For me, the problem is that I don't have a good sense of what the concrete definition of a Lie algebra is supposed to be.

I suspect that a good concrete definition of a Lie algebra is as a space of derivations on some algebra closed under commutator. In that case, is it correct to say that a Lie algebra acts faithfully as derivations on its universal enveloping algebra? Is this a good analogue of Cayley's theorem?

(Motivation: in the books on Lie algebras I have read, the authors verify that Lie algebras which occur in nature satisfy alternativity and the Jacobi identity, but I have never seen any simple justification that these axioms are "enough" in the same way that Cayley's theorem tells you that the axioms for a group or a ring are "enough." There is just Ado's theorem which, again, comes with qualifications and is hard.)

Here is a way of avoiding Ado's theorem, at the expense of using the Poincare-Birkhoff-Witt Theorem. The PBW theorem has no finite dimensionality or characteristic hypotheses, so you may like this better. Note, however, that I will realize finite dimensional Lie algebras as endomrophisms of infinite dimensional vector spaces.

Let's define a concrete Lie algebra to be a vector space $V$, and a vector subspace $\mathfrak{h}$ of $\mathrm{End}(V)$ closed under commutator.

Theorem: Every Lie algebra is isomorphic to a concrete Lie algebra.

Proof: Let $\mathfrak{g}$ be a Lie algebra and $U$ its universal enveloping algebra. The Lie algebra $\mathfrak{g}$ acts on $U$ by left multiplication, so this gives a map $\mathfrak{g} \to U$ taking bracket to commutator. We must prove this map is injective.

Choose a basis ${ v_i }$ for $\mathfrak{g}$. Suppose that left multiplication by $\sum a_i v_i$ is $0$. Then $\left( \sum a_i v_i \right) \cdot 1 = \sum a_i v_i$ would be zero in $U$. But, by the PBW theorem, the $v_i$ are linearly independent in $U$, a contradiction. QED

As far as I know, this special case of PBW is as hard as the whole theorem.

A finite-dimensional real Lie algebra always arises as the Lie algebra of a Lie group. Of course, the proof of this does use Ado's theorem, as well as some Lie group theory (a subalgebra of a Lie algebra of a Lie group $G$ is also a Lie algebra of a Lie group, but not necessarily the Lie algebra of a closed subgroup of $G$). The upshot is that over $\mathbb{R}$ the definition of (finite-dimensional) Lie algebra suffices to deal with all Lie groups.