Prove that formula is satisfiable in some infinite structure, but invalid in all finite structures Given formula.
$$[\forall x \exists y P(x,y) ]\;\land [\forall x \forall y (P(x,y) \to \lnot P(y,x))] \;\land [\forall x \forall y \forall z ((P(x,y) \land (P(y,z)) \to P(x,z)))]$$
First of all, I tried to find some (infinite) interpretation, where this formula becomes true. While looking at this formula, I noticed that the second part of it is anti-symmetric relation, and the third part is transitivity. So I immediately thought about choosing P as a partial order on natural numbers.
Let $M = \mathbb{N}$ and $P(x,y) := x < y$.
If I choose $y = x + 1$ in the first part, then the formula evaluates to T
OK, if everything is good till this moment, then let's try to prove that the statement is identically F for any finite interpretation.
I'm stuck for a few hours in the second part. Had an idea to blindly 'rename' each sub-formula by some letter, and try to prove it using propositional calculus methods (proof by contradiction or just via truth tables). But the first one $\forall x \exists y P(x,y)$ which involves $\exists$ quantifier confused me.
What did I missed here? Doing self study of material is very time consumable when you're stuck. An answer with detailed explanation will be much valuable.
Thank you.
 A: The idea is the following : $P$ is interpreted as a relation that is transitive and antisymmetric, in other words, a strict ordering $<$.
But the first part of the formula in question also says the following : there is no maximal element, in other words, for every element, there is a strictly bigger one. 
If you have such an interpretation, pick an element $x_0$. Then it's not maximal, so there must be $x_1>x_0$. Similarly, there must be $x_2>x_1$. Proceed on, with induction to create $x_n$ for all $n\in \mathbb{N}$. If $n<m$, then $x_< x_{n+1}<...< x_m$, and so out of transitivity, $x_n < x_m$, and so if $n\neq m$, $x_n\neq x_m$. Now can you have a finite interpretation and such a sequence in it ?
A: I like to think about this visually/graphically. So think about any $P(x,y)$ relation as there being an arrow from $x$ to $y$.
Because of the relation being asymmetical and transitive, you can never have a cycle of arrows, and therefore we are able to arrange all objects in the domain such that every arrow will go from left to right.
But if the domain is finite, then there must be one or more right-most objects, meaning that they don't have an outgoing arrow ... but that contradicts the first conjunct that requires every object to have an outgoing arrow. So, it is impossible to satisfy this with a finite domain.
A: If $\Bbb M$ is any interpretation let $P^M=\{(x,y)\in M: \Bbb M\text { satisfies } P(x,y)\}$ then $P^M$ is a binary relation on $M.\;$(I.e. $P^M$ is a subset/subclass of $M\times M.$). 
Let $\Bbb M$ be a finite interpretation with $n$ members ($n\in \Bbb N$). Suppose $P^M$ satifies the first condition (I.e. the domain of $P^M$ is $M$) and that $P^M$ is transitive. Then $P^M$ cannot be anti-symmetric because $\exists x\;(P^M(x,x)).$ 
Proof: Take $x_1\in M$ and for $1\leq j\leq n$ let $x_{j+1}\in \{y\in M: P^M(x_j,y)\}.$ There exist $i,j$ with $1\leq i<j\leq n+1$ with $x_i=x_j$ by the Pigeon-Hole Principle.  Now  transitivity of $P^M$ implies, by induction on $k$, that  $P^M(x_i,x_{i+k})$ whenever $1\leq k\leq n+1-i.$  But then we have $P^M(x_i,x_j)$ and $x_i=x_j,$ contradicting anti-symmetry.
Remark: If you prefer, let $M=\{m_i:1\leq i\leq n\},$ and let $x_1=m_1$ and let $x_{j+1}=m_u(j)$ where $u(j)=\min \{v: P^M(x_j,m_v\}$, if you want a  recursive algorithm for defining  each $x_j$.
