For example, how can I rewrite $$\forall a\exists b\exists c\exists d\forall e\left({a\ne b\wedge a\ne c\wedge a\ne d\wedge b\ne c\wedge b\ne d\wedge c\ne d\wedge P\left({e,a}\right)}\right)$$ into a simpler form, where I just want to show that $a$, $b$, $c$ and $d$ are mutually/pairwise different?
I think one way is to write $$\forall a\exists b\exists c\exists d\forall e\left({\left|{\left\{{a,b,c,d}\right\}}\right|=4\wedge P\left({e,a}\right)}\right),$$ but I wonder if it's legit to use notations from set theory in propositional logic, and if there are any other ways.
If the language you are using has $\neq$ as a symbol (a lot of texts use only $=$ and you have to write $\lnot(a=b)$ instead of $a \neq b$) then AFAIK the only way to stay within logic and your language is indeed to assert an explicit $a \neq b$ for every unordered pairs $\{a,b\}$, so for $4$ variables we need $\binom{4}{2}=6$ such statements in conjunction (so with $\land$ between them), as you have done.
If you're allowed to do so, you could introduce a new $4$-ary predicate by an abbreviation, so e.g. $$ D(x,y,z,u) := \lnot(x = y) \land \lnot(x = z) \land \lnot(x = u) \land \lnot(y = z) \land \lnot(y = u) \land \lnot(u = v) $$ (using the strict interpretation) and then writing your statement as
$$\forall a\exists b\exists c\exists d\forall e: D(a,b,c,d) \land P(e,a)$$
if brevity is what you're after.