In the context of formal logic, such will usually not consist of a proof... or more perhaps more clearly, a formal proof. It will "show" that iff (P ⟹ Q), then (~Q ⟹ ~P) comes as valid. For informal logic settings, that will usually suffice, and it could suffice as an argument of some sort in a formal logic setting given that you've already established the completeness metatheorem of classical propositional logic. However, it does not consist of a formal proof, since in formal logic, a formal proof gets defined something like "a sequence of well-formed formulas (often just called "formulas") such that every well-formed formula is either an axiom, a hypothesis made under a certain scope which will get discharged eventually, or a well-formed formula permissible according to the rules of inference and well-formed formulas already in the proof." What you've given above, does not give us such a sequence of well-formed formulas.
A propositional sentence, built out of propositional atoms, does indeed describe a set: namely, the set of valuations making it true. Remember that a valuation is just a map from the set of atoms to $\{$True, False$\}$ (such a map extends to a map from the set of all propositional sentences to $\{$True, False$\}$ via an appropriate recursion). Valuations in propositional logic serve the same semantic role as models in predicate logic: a propositional sentence is true, or false, with respect to a given valuation, and different valuations make different things true or false.
For $\varphi$ a propositional sentence, let $Set(\varphi)$ be the set of valuations making $\varphi$ true. Think of $Set(\varphi)$ as describing the conditions under which $\varphi$ is true: a smaller set corresponds to a more demanding sentence. For example, suppose I have two sentences, $\varphi$ and $\psi$. Then we have $$Set(\varphi\implies\psi)=Set(\neg\varphi)\cup Set(\psi),$$ since a valuation satisfies $\varphi\implies \psi$ iff it either satisfies $\neg\varphi$ or it satisfies $\psi$.
Note that this means that the Boolean propositional operations (conjunction, disjunction, negation, ...) correspond as desired to Boolean set operations (intersection, union, (relative) complementation, ...). So this does indeed give a set-theoretic interpretation of propositional logic.
Now let's look at Venn diagrams.
Venn diagrams are visual representations of the $Set(-)$ operation - or rather, they are a pictorial language for making assertions about the valuation sets assigned to propositional sentences. E.g. when we draw one circle wholly inside another, we're asserting that every valuation making the first circle's sentence true also makes the second circle's sentence true. Crucially, a "point on the plane" in a Venn diagram represents a valuation.
Keep in mind that the assertion made by a specific diagram may or may not be correct - it's always possible to write something meaningful but wrong.
But suppose I've gone ahead and done that: I have two propositional sentences $\varphi$ and $\psi$, and I've drawn circles $C_\varphi$ and $C_\psi$ representing them each respectively, and I've drawn $C_\varphi$ wholly inside $C_\psi$. That drawing is correct iff every valuation making $\varphi$ true also makes $\psi$ true. That statement in turn is true iff there are no valuations which make $\varphi$ true but $\psi$ false, and that statement's truth is equivalent to the claim that $(\neg\varphi)\vee\psi$ is true under every valuation - and that in turn is the assertion made by the Venn diagram which represents $(\neg\varphi)\vee\psi$ as everything.
Best Answer
Yes, for example you can use DeMorgan's laws: $$a \vee b = \neg((\neg a) \wedge (\neg b))$$ $$a \wedge b = \neg((\neg a) \vee (\neg b))$$
As well as distributivity over the operators:
$$a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c) $$ $$a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c) $$
And there are a lot of more rules you can use to simplify expressions.