First my apologies if this question has been asked before.
Exposition
I'm new at learning how to prove theorems and among the given exercises from my reference material it is asked to prove the following:
The original question in words:
For every positive $x \in \mathbb{Q}$, there exists positive $y \in \mathbb{Q}$ for which $y \lt x$.
I translated it and got:
$\forall x \in \mathbb{Q}_{\gt0} \ \exists y \in \mathbb{Q}_{\gt0}, \ y \lt x$
Here is my attempted proof.
If $x \in \mathbb{Q}_{\gt0}$ then $\exists y \in \mathbb{Q}_{\gt0}$ such that $y \lt x$. Suppose $\forall y \in \mathbb{Q}_{\gt0}$, $y \geq x$.
So if $y \in \mathbb{Q}_{\gt0}$ then $y \geq x$. By contrapositive if $y \lt x$ then $y \notin \mathbb{Q}_{\gt0}$.
But this doesn't make sense. Hence we were wrong to assume that $\forall y \in \mathbb{Q}_{\gt0}$.
Question
I'm having trouble with the part starting from this doesn't make sense. I looked at the $y \notin \mathbb{Q}_{\gt0}%$ and made a somewhat educated guess regarding the fact that $y \notin \mathbb{Q}_{\gt0}%$ doesn't logically follow from the premise that $y \lt x$. This in the sense that the less than 'operator' can only be defined between two mathematical objects of the same kind.
Is there something i got wrong? Does this make sense? Is the proof complete anyway? What would be the correct proof?
In clear and concise terms, I'm trying to understand if my proof is correct.
Thanks
UPDATE
I re-read the question again from the material and $y$ is supposed to be a positive rational too. Yet i think given replies at the original time of this update still apply.
UPDATE 2
With regards to the answer provided by @crf i think i should provide the proof strategy. By this point if someone could see something wrong in the proof, i guess it came from me making something wrong in my strategy. So here is the proof strategy. All that follows of course is supposed to be part of draft work.
1. First i get the statement into symbolic form in order to 'safely' transform the expression:
$\forall x \in \mathbb{Q}_{\gt0} \ \exists y \in \mathbb{Q}_{\gt0}, \ y \lt x$
2. Transform the obtained statement into conditional form:
We know that $\forall x \in S, \ Q(x)$ is equivalent to $(x \in S) \Rightarrow Q(x)$.
Then we get:
$x \in \mathbb{Q}_{\gt0} \Rightarrow \exists y \in \mathbb{Q}_{\gt0}, \ y \lt x$
Reference: Book of proof by Richard Hammack, pp 54, Fact 2.2 available online here
3. Then we attempt a proof by contradiction for this conditional statement:
As such our hypotheses become:
$$
x \in \mathbb{Q}_{\gt0} \\ \forall y \in \mathbb{Q}_{\gt0} \ (y \geq x)
$$
And this is equivalent to :
$$
x \in \mathbb{Q}_{\gt0} \\ y \in \mathbb{Q}_{\gt0} \Rightarrow y \geq x
$$
and conclusion: will be a contradiction
4. Transform $\forall y \in \mathbb{Q}_{\gt0} \ (y \geq x)$ to get its contrapositive:
We get as new hypotheses:
$$
x \in \mathbb{Q}_{\gt0} \\ y \lt x \Rightarrow y \notin \mathbb{Q}_{\gt0}
$$
That where i got stuck and i started guessing: how does $y \notin \mathbb{Q}_{\gt0}$ follow from $y \lt x$? I couldn't see a rigorous contradiction between that and premises and got got stuck!
Thanks for bearing all this!