Difficulty in proving the existence of one-way functions By definition:

A polynomial-time computable function $f:$ $\{$0,1$\}$$^*$→ $\{$0,1$\}$$^*$ is a one-way function if for every probabilistic polynomial time Turing Machine $PTM$ there is a neglegibible function $E$ $:$$\mathbb{N}  → \mathbb{N} $
  $ \ s.t. \ $ $Pr$ $x$ $∈$ $\{$0,1$\}$$^n$ $[PTM \ \ inverts \ \ f(x)] ≤ E(n)$.

Now, reading the definition above, the existence of one-way functions seems like an easy bet, however it is considered a stronger assumption than $P \neq NP$.
Apparently proving the existence of these functions would be more difficult than proving $P = NP ?$   And I'd like to know the technical reasons for this, does it have something to do with the "for every" in the definition? 

What steps would a mathematician or computer scientist take to prove that one-way functions exist? I believe that since proving its existence would also prove $P \neq NP$, this means that we cannot use the techniques that we know for sure does not work: Relativization, diagonalization, Natural Proof.

So,  what form could such a proof take? Maybe something in  second(+)-order logic?
Apparently proving the existence of these functions would be more difficult than proving $P\not =NP$? And I'd like to know the technical reasons for this, does it have something to do with the "for every" in the definition?


The answer is in your question itself:


  I believe that since proving its existence would also prove $P\not =NP$


This is indeed the case. Somebody that proves the existence of one-way functions automatically also proves $P\not = NP$. On the other hand, it is conceivable that you could prove $P\not = NP$ without proving that one way functions exist. Thus, proving the existence of one-way functions is at least as hard as proving $P\not = NP$.


  What steps would a mathematician or computer scientist take to prove that one-way functions exist?


Coming up with an extremely clever and creative idea that nobody came up with before.