Formal proof of implication I am currently stuck on this particular task. I need to formally prove that
(∃a ∀b (b<a)) → (∀a ∃b (a<b))

Now, what I have so far is that I need to prove that the above implication is a tautology, and that my premises are (∃a ∀b (b<a)) A and (∀a ∃b (a<b)) B.
I am not sure where to go next...
I tried assuming that A is True.
Next I assume that A→B is True.
Using Modus Ponens if A and A→B are True I can prove B.
Therefore, if A and B are True the implication of both must be True.
But I am not convinced this works.
Alternatively I tried assuming A is true.
If A is true it means ∃a ∃b (b<a) is also true.
That means there must be a b that satisfies the same condition? If a and bare swapped? So ∃a ∃b (a<b)? and then somehow deduce ∀a ∃b (a<b)?
Any help would be appreciated, thanks!
 A: I will assume you are stating this for real numbers (that is to say, you omit to write "$\in \Bbb R$" in the quantifiers). Suppose that A is true, so that there exists a number $a$ such that for every number $b$ the relation $b<a$ holds; if $c$ is any number, then $c<a$ hence B holds. So, A implies B as desired.
A: When you have to prove that some sentence of the form "$(\forall x\in X)\,P(x)$, you should start by : "Let $x$ be some element of $X$, let's prove $P(x)$".
Here, suppose "$(\exists a_0)(\forall b)\, b<a_0$" is true. Let's prove "$(\forall b) (\exists a)\, b<a$" (I changed the letters, to simplify the proof).
So let $b$ be some element. The $a_0$ given by the hypothesis is now a good candidate for the conclusion : let $a=a_0$, we have $b<a$, so that the conclusion is true.
What you have to understand is that in "$(\exists a)(\forall b)\, P(a,b)$", the "$a$" is the same for every $b$. In "$(\forall b) (\exists a)\, P(a,b)$", $a$ is dependent on $b$ : you can chose it after $b$ has been given.
One final note : your "$<$" relation is quite odd : of all the $b$ that must verify $b<a$, there is in particular $a$, so $a$ should verify $a<a$. Maybe a bad notation ? At least a confusing one :-)
A: Assume $$\tag1\exists a\forall b(b<a).$$ 
Accordingly, let $a_0$ such that $$\tag2\forall b(b<a_0).$$ 
We want to show (based on the hypothesis $(1)$) that $\forall a\exists b(a<b)$. So let $a$ be arbitrary. By specialization from $(2)$, we have $a<a_0$. So by letting $b=a_0$, we have $a<b$, i.e., $\exists b(a<b)$. As $a$ was arbitrary, we showed $$ \forall a\exists b(a<b).$$
As all this happend under the hypothesis $(1)$, we have
$$\exists a\forall b(b<a)\to\forall a\exists b(a<b). $$
A: 
I tried assuming that A is True. Next I assume that A→B is True.

That is clearly awry. Never assume the thing that you want to prove. You should assume 
$A$ then derive $B$ under that assumption, so that you may deduce that $A→B$ holds.

Alternatively I tried assuming A is true. If A is true it means $∃a ∃b (b<a)$ is also true. That means there must be a b that satisfies the same condition? If a and b are swapped? So $∃a ∃b (a<b)$? and then somehow deduce $∀a ∃b (a<b)$?

Not quite.  You don't derive an existance from an universal.
But the technique you need is alpha-replacement.   We can safely substitute the bound term with any token that does not already occur within the scope of the quantifier.   So think of it as proving $\exists a~\forall b~(b<a)\to \forall b~\exists a~(b<a)$ then juggling the letters.


*

*Begin


*

*Assume $\exists a~\forall b~(b<a)$


*

*Let $y$ be an arbirary term. 


*

*Let $x$ be a witness for the assumption.

*$\forall b~(b<x)$ via instantiation of existential bound $a$ to witness $x$.

*$y<x$ via instantiation of universal bound $b$ to arbitrary $y$.


*$\exists b~(y<b)$ via generalisation of witness $x$ to existential bound $b$.


*$\forall a~\exists b~(a<b)$ via generalisation of arbitrary $y$ to universal bound $a$


*Done: $\exists a~\forall b~(b<a)\to \forall a~\exists b~(a<b)$
