How can the logical validity of the following argument be proved?
$$\forall x\mathbb P(x, x)\wedge\forall x\forall y(\mathbb P(x, y)\rightarrow\forall z(\mathbb P(x, z)\vee\mathbb P(y, z)))\rightarrow\forall x\forall y(\mathbb P(x, y)\vee\mathbb P(y, x))$$
I have thought of using the Tableaux but I am a beginner in discrete maths. Can anyone help?
A Tableau proof will do:
1) $∀xP(x,x) ∧ ∀x∀y(P(x,y) → ∀z(P(x,z) ∨ P(y,z)))$ --- premise
2) $\lnot ∀x∀y(P(x, y) ∨ P(y, x))$ --- negation of the conclusion
3) $\lnot (P(a, b) ∨ P(b, a))$ --- from 2): $a$ and $b$ new
4) $\lnot P(a, b)$ --- from 3)
5) $\lnot P(b,a)$ --- from 3)
6) $P(a,a)$ --- from 1)
7) $P(a,a) → ∀z(P(a,z) ∨ P(a,z))$ --- from 1)
8a) $\lnot P(a,a)$ --- left branch from 7), using $\to$-rule: closed with 6)
8b) $∀z(P(a,z) ∨ P(a,z))$ --- right branch from 7), using $\to$-rule
9) $P(a,b) ∨ P(a,b)$ --- closed with 4).