Is this a valid proof? If so can someone explain it?
Prove that: $\forall x: \exists y : (x \leq y) \land \lnot I(y)$
Premises: $\forall x: \forall y: [I(x) \land \lnot I(y)] \implies (x \lt y)$ and $\exists z : \lnot I(z)$
Proof: We let $a$ be an arbitrary element. Then $I(a) \lor \lnot I(a)$.
Case 1: $I(a)$ By rules of instantiation and our second premise we instantiate b such that $\lnot I(b)$. $I(a) \land \lnot I(b)$ so by modus ponens and our first premise, $a \lt b$ and by our definition of $\leq$, $a \leq b$. Therefore $(a \leq b) \land \lnot I(b)$. Then by existence, $\exists y : (a \leq y) \land \lnot I(y)$.
Case 2: $\lnot I(a)$ We know $a = a$, so by definition $a \leq a$. We assumed $\lnot I(a)$, so using conjunction we have $(a \leq a) \land \lnot I(a)$. Thus by existence $\exists y : (a \leq y) \land \lnot I(y)$.
Then in both cases, by generalization, we have $\forall x: \exists y : (x \leq y) \land \lnot I(y)$.
For case 2: if we took $a$ as arbitrary why did we use rule of existence and not generalization?
Your proof is exactly correct! Well done.
And you used existential introduction in both cases exactly because you were trying to prove an existential: $\exists y (a \leq y \land \neg I(y))$
It's only after that proof by cases that you introduce a universal ... which is why you introduced $a$ as an arbitrary object.
Yes, it may feel weird that in case $2$ you end up creating the existential using the same object as that you end up creating the universal at the end with ... this is certainly unusual for a proof ... but it is all perfectly valid!
Indeed, when the statement says: $\forall x \exists y ...$, then of course for some of the $x$'s the $y$ could be the same as the $x$ ... and that's exactly what is going on here.