I have a question regarding models of set theory.
As the title say I am trying to prove that $(V_{\omega},\in)\models ZFC-Inf+\neg Inf$, that is $V_\omega$ is a model for all the $ZFC$ axioms except from the axiom of infinity, where it is a model of its negation.
Now, I think I proved everything right except from the axiom schema of replacement and the axiom of choice, where I don't really know where to start. Can you guys help me here?
Also, I am not entirely sure of the proof I gave for the Axiom Schema of Separation. Here's what I did. Given any formula $\phi(x)$ and any $a\in V_{\omega}$, I need to check that $B:=\{c\in a : \phi^{V_{\omega}}(c)\}$ is a set, i.e. an element of $V_{\omega}$. Now, $a\in V_{\omega}$ implies that $a\in V_n$ for some $n\in\omega$. We have now that $B\subseteq a\in V_n$, by transitivity of $V_n$ we conclude that $B\subseteq V_n$, but this implies that $B\in V_{n+1}$ and so $B\in V_{\omega}$ and this concludes the proof. Is that correct?
Axiom of Choice: This is a special case of a theorem of $\mathbf{ZF}$ that says that if $X$ is a finite set of non-empty sets, there exists a choice function $f:X\to \cup X$ such that $f(z)\in z$ for all $z\in X$. It is proved by induction on $n=|X|$. If $X=\emptyset$ there is nothing to do. Else, assume there is a choice function for all sets of size $n$. Let $X$ be a set of size $n+1$. Take any $x_0\in X$ and let $X'=X\setminus\{x_0\}$. Then $|X'|=n$. By the induction hypothesis there is a function $f_{X'}$ with domain $X'$ such that $f_{X'}(z)\in z$ for all $z\in X'$. Now take some $y_0\in x_0$ and let $f_X=f_{X'}\cup\{(x_0,y_0)\}$. Then $f_X$ is a choice function on $X$.
For a set $X\in V_\omega$, $X$ is hereditarily-finite, so $|X|\in\omega$, and you can apply the theorem above to get a choice function. Since $X$ is hereditarily finite, all members of the transitive closure of $X$ are members of $V_\omega$, so a choice function built this way stays entirely in $V_\omega$.
Axiom schema of Replacement: This is similar to separation, but slightly more complicated. Say you have a formula $\varphi(x,y,p_1,\dots,p_n)$ whose free variables are among $x,y,p_1,\dots,p_n$ and a set $X\in V_\omega$ such that $$(V_\omega,\in)\models \forall x,y_1,y_2 (x\in X\land\varphi[y_1/y]\land\varphi[y_2/y]\rightarrow y_1=y_2)$$ Then $$(V,\in)\models \forall x,y_1,y_2(x\in V_\omega\land y_1\in V_\omega\land y_2\in V_\omega \land x\in X\land\varphi^{V_\omega}[y_1/y]\land\varphi^{V_\omega}[y_2/y]\rightarrow y_1=y_2)$$ Now, using that $X\subseteq V_\omega$, letting $\psi = \varphi^{V_\omega} \land y\in p_{n+1}$ and assigning the additional parameter $p_{n+1}$ to take on the value $V_\omega$ we can conclude $$(V,\in)\models \forall x,y_1,y_2 (x\in X\land\psi[y_1/y]\land\psi[y_2/y]\rightarrow y_1=y_2)$$ Now we use Replacement globally on $(V,\in)$ to conclude $$(V,\in)\models \exists B\forall y(y\in B\leftrightarrow \exists x (x\in X\land \psi))$$ The set $B$ obtained this way satisfies the requirement of the axiom schema of Replacement for $\varphi$ relative to $(V_\omega,\in)$.
Axiom of Separation: I agree with your proof.