Theorem: Axiom of Specification from Replacement and Empty Set

The {{axiom-link|Specification|Sets}} is a consequence of:
:the {{axiom-link|Replacement}}
and
:the {{axiom-link|the Empty Set|Set Theory}}.

Proof:
{{Proofread|proof is tedious}}
Let $A$ be an arbitrary set.
Let $\map P x$ be an arbitrary propositional function.
It is to be shown that there exists a set $B$ consisting of exactly the $y \in A$ such that $\map P y$.
That is:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
By Law of Excluded Middle, there are two choices:
:$\exists y \in A : \map P y$
or:
:$\not \exists y \in A : \map P y$
Suppose $\not \exists y \in A : \map P x$.
By {{axiom-link|the Empty Set|Set Theory}}, take $B = \O$.
Take arbitrary $A$ and $y$.
Assume $y \in B$.
This contradicts the empty set definition.
By Rule of Explosion, we have:
:$y \in A \land \map P y$
giving:
:$y \in B \implies \paren {y \in A \land \map P y}$
Now assume:
:$y \in A \land \map P y$
This contradicts our assumption that:
:$\not \exists y \in A : \map P y$
By Rule of Explosion, we have:
:$y \in B$
giving:
:$\paren {y \in A \land \map P y} \implies y \in B$
Thus:
:$\paren {y \in A \land \map P y} \iff y \in B$
and by Universal Generalisation and Existential Generalisation:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
This shows that the {{axiom-link|Specification|Sets}} holds when:
:$\not \exists y \in A : \map P y$
{{qed|lemma}}
Suppose $\exists y \in A : \map P y$.
Take some fixed $w \in A : \map P w$.
Define the propositional function $\map Q {x, z}$ as follows:
:$\paren {\map P x \land z = x} \lor \paren {\neg \map P x \land z = w}$
Usually this would be written as the mapping:
:$\map f x = \begin {cases}
x & : \map P x \\
w & : \text{otherwise}
\end {cases}$
It is to be shown that $\map Q {x, z}$ determines a mapping.
That is:
:$\forall x: \exists a: \forall z: \paren {\map Q {x, z} \iff a = z}$
Take arbitrary $x$ and $z$.
Assume that $\map Q {x, z}$, giving:
:$\paren {\map P x \land z = x} \lor \paren {\neg \map P x \land z = w}$
By Law of Excluded Middle, there are two choices:
:$\map P x$
or:
:$\neg \map P x$
Suppose $\map P x$.
{{AimForCont}} that:
:$\paren {\neg \map P x \land z = w}$
Then we have the contradiction:
:$\map P x \land \neg \map P x$
Thus we have:
:$\neg \paren{\neg \map P x \land z = w}$
and by Modus Tollendo Ponens:
:$\paren {\map P x \land z = x}$
Take $a=x$.
Thus, for all $z$ such that $\map Q {x, z}$, we have $a = x = z$, giving:
:$\map Q {x, z} \implies a = z$
Suppose $\neg \map P x$.
{{AimForCont}} that:
:$\paren {\map P x \land z = x}$
Then we have the contradiction:
:$\map P x \land \neg \map P x$
Thus we have:
:$\neg \paren {\map P x \land z = x}$
and by Modus Tollendo Ponens:
:$\paren {\neg \map P x \land z = w}$
Take $a=w$.
Thus, for all $z$ such that $\map Q {x, z}$, we have $a = w = z$, giving:
:$\map Q {x, z} \implies a = z$
Thus:
:$\map Q {x, z} \implies a = z$
follows from both $\map P x$ and $\neg \map P x$.
By Universal Generalisation and Existential Generalisation:
:$\forall x: \exists a: \forall z: \paren {\map Q {x, z} \iff a = z}$
and $\map Q {x, y}$ determines a mapping.
{{qed|lemma}}
We now have a propositional function $\map Q {x, y}$ satisfying the premise of {{axiom-link|Replacement}}, giving:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \exists x \in A : \map Q {x, y} }$
By definition of $\map Q {x, y}$, we have:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \exists x \in A : \paren {\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w} } }$
where $w \in A$ and $\map P w$.
We must show that the {{axiom-link|Specification|Sets}} holds:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
Assume $y \in B$.
By the {{axiom-link|Replacement}}, we have:
:$\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w}$
for some $x \in A$.
$\map P x \land y = x$ and $x \in A$ imply $y \in A \land \map P y$.
Recalling that $w \in A$ and $\map P w$, $\neg \map P x \land y = w$ implies $y \in A \land \map P y$.
Thus:
:$y \in B \implies \paren {y \in A \land \map P y}$
Now assume $y \in A \land \map P y$.
Then there is an $x$, namely $x = y$, such that:
:$\exists x \in A : \paren {\map P x \land y = x}$
By Rule of Addition:
:$\exists x \in A : \paren {\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w} }$
Thus, by the {{axiom-link|Replacement}} we have $y \in B$.
Thus:
:$\paren {y \in A \land \map P y} \implies y \in B$
This completes the biconditional:
:$y \in B \iff \paren {y \in A \land \map P y}$
By Universal Generalisation and Existential Generalisation:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
This shows that the {{axiom-link|Specification|Sets}} holds when:
:$\exists y \in A : \map P y$
{{qed|lemma}}
Thus, the {{axiom-link|Specification|Sets}} holds both when:
:$\exists y \in A : \map P y$
and when:
:$\not \exists y \in A : \map P y$
completing the proof.
{{qed}}
Category:Zermelo-Fraenkel Axioms
Category:Empty Set
khoxbbvh8129avon0hn9bzk699p05p9