Yes, you can remove the axiom of foundations by the same argument: move from a universe of $\sf ZF-Fnd$ to the von Neumann universe, which is the largest well-founded and transitive class.
When you remove Infinity, Power set, or Replacement, you get strictly weaker theories. To see why, note that $V_\omega,\mathrm{HC}$ and $V_{\omega+\omega}$ are models of $\sf ZF-Infinity, ZF-Power, ZF-Replacement$ respectively. Therefore $\sf ZF$ proves these theories have a model, so they are consistent. In particular by Gödel's theorem none of them can prove that $\sf ZF$ itself is consistent.
I haven’t read this work of Jech, but it seems you are under a few misconceptions.
Replacement is not indexed by “all functions”. A function is an object discussed in ZFC, so it does not make sense to say there is one axiom per function. Instead, replacement is indexed over “properties” in the same way separation is.
Formally, consider any formula $P(x, y, w_1, \ldots, w_n)$ - that is, a formula $P$ in the language of set theory such that every variable which occurs free in $P$ is one of $x, y, w_1, \ldots$, or $w_n$. The instance axiom of replacement for $P$ states
$$\forall w_1 \cdots \forall w_n \forall a (\forall x \in a \exists! y P(x, y, w_1, \ldots, w_n) \implies \exists b \forall y (y \in b \iff \exists x \in a P(x, y, w_1, \ldots, w_n)))$$
It is clear that because there are only countably many such $P$, there are only countably many instances of replacement. It is also clear that deciding whether a particular sentence is an instance of the axiom scheme of replacement is decidable. The same is true for deciding whether a sentence is an instance of the axiom scheme of separation. Therefore, whether a sentence is an axiom of ZFC is decidable.
For the rest of the discussion, we assume ZFC is consistent.
We can encode sentences in the language of arithmetic into the language of set theory in such a way that makes ZFC an extension of Peano Arithmetic. Because ZFC is a recursively axiomatisable consistent extension of Peano Arithmetic, there is no algorithm which can decide whether a particular sentence can be proved in ZFC.
Finally, ZFC cannot be finitely axiomatised. There is a powerful principle called the “reflection principle”, which states that for all sentences $\phi$, ZFC proves that there is some transitive set $S$ such that $(S \models \phi) \iff \phi$. So for any list $A_1, \ldots, A_n$ of axioms of ZFC, we can prove in ZFC that there is some model of $\phi := A_1 \land A_2 \land \cdots \land A_n$, and thus the combination of axioms $A_1, \ldots A_n$ is consistent. If ZFC were finitely axiomatisable, then it would prove itself consistent, which is impossible by Gödel’s second incompleteness theorem.
So the set of axioms of ZFC is countably infinite and decidable, and we can’t cut the axioms down to a nice finite list while still having all the theorems of ZFC.
Best Answer
The idea of a schema is to replace a second-order idea by a template for axioms. So the natural thing is to also have a template for a proof.
Different Separation axioms have different proofs, since mostly they rely on different Replacement axioms to be proven. But we have a recipe, a template, an algorithm, that given any axiom in the Separation schema, we can prove that axiom.
Since the whole debate here is meta-mathematical anyway, that quantification which happens in the meta-theory is just that. Or, if you will, if this wasn't the case, there would be some Separation axiom $\varphi$ which cannot be proved from $\sf ZFC$, but plugging it into our template does work. So that's not the case.
As for your other question, deriving a contradiction is merely a proof that $\exists x(x\neq x)$. It's a finite proof, there are finitely many axioms from $\sf ZFC+\phi$ appearing in it. One of these axioms, presumably is your $\phi$, but the rest are just a finite list of axioms from $\sf ZFC$.