Proof using predicate logic to show subsets from axiom schema of specification are unique

Question

I would like to prove that axiom of specification and axiom of extensionality implies that set constructed from axiom of specification is unique. I understand the arguments given by words but I would like to practice and prove it using predicate logic and inference rules.

I would be happy if you could help or hint me about how to prove a specific part that I am stuck with. I will show you my reasoning below. I would also appreciate if there would be some comments on how to make proof easier or more readable.

I want to show that for all formula $\phi$ assumptions $\forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ and $\forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ prove that $\forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$.

My sketch of the proof proceeds as follows.

$1. \forall w_1, ..., w_n: \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (premise)

$2. \forall x: \exists y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 1)

$3. \exists y : \forall z: (z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (universal instantiation from 2)

$4. \forall z: (z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $b$)

$5. \forall z: (z \in c \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (existential instantiation from 3 for some $c$)

$6. d \in b \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 4)

$7. d \in c \iff (d \in a \land \phi(w_1, ..., w_n, d))$ (universal instantiation from 5)

$8. d \in c \iff d \in b$ (modus ponens on 6 and 7 using the following tautology: $(p \iff q) \land (q \iff r) \to (p \iff r)$)

$9. \forall z: (z \in c \iff z \in b)$ (universal generalization from 8 because $d$ was arbitrary)

$10. \forall x: \forall y: (x = y \iff (\forall z:( z \in x \iff z \in y)))$ (premise)

$11. \forall y: (c = y \iff (\forall z:(z \in c \iff z \in y)))$ (universal instantiation from 10)

$12. c = b \iff (\forall z: (z \in c \iff z \in b))$ (universal instantiation from 11)

$13. c = b$ (modus ponens from 9 and 12 using the following tautology: $p \land (p \iff q) \to q$)

Here is the point I get stuck because I would like to prove for uniqueness that $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z)) \to r = b$ but from step 13 I (at least I think so) can prove only existence because $b$ and $c$ were not arbitrary but specifically chosen (kind of).

Let us assume that I have proven $\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b)$ as step 100.

$101. \forall z:(z \in b \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = b))$

(modus ponens from 4 and 100)

$102. \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$

(existential generalization of 101)

$103. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \iff \exists y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z))) \land(\forall r: ( \forall z:(z \in r \iff (z \in a \land \phi(w_1, ..., w_n, z))) \to r = y))$

(tautology due to the definition of "exists unique")

$104. \exists! y: \forall z:(z \in y \iff (z \in a \land \phi(w_1, ..., w_n, z)))$ (modus ponens from 103 and 104 using the following tautology: $p \land (p \iff q) \to q$)

$105. \forall x: \exists! y: \forall z:(z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 104 due to the fact that $a$ was arbitrary)

$106. \forall w_1, ..., w_n: \forall x: \exists! y : \forall z: (z \in y \iff (z \in x \land \phi(w_1, ..., w_n, z)))$ (universal generalization of 105 due to the variables $w_1, ..., w_n$ being arbitrary)

This completes the proof. Any suggestions are very welcomed.

Answer 1

An attempt to re-structure the proof...

1. $∀x ∃y ∀z (z∈y⟺(z∈x ∧ ϕ(z)))$ --- axiom

2.-3. $∃y ∀z (z∈y⟺(z∈a ∧ ϕ(z)))$ --- universal instantiation from 1

4. $∀z (z∈b⟺(z∈a ∧ ϕ(z)))$ --- existential instantiation from 3, for some $b$

4a. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- new premise

5. $∀z(z∈c⟺(z∈a∧ϕ(z))) ∧ d≠b$ --- existential instantiation from 4a, for some $c$

5a $∀z(z∈c⟺(z∈a∧ϕ(z)))$ --- from 5. by taut: $(p \land q) \to p$ and mp

5b. $c≠b$ --- from 5. by taut: $(p \land q) \to q$ and mp

5c. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to \lnot (c=b)$ --- from 5b by taut: $p \to (q \to p)$ and mp

6. $d∈b⟺(d∈a ∧ ϕ(d))$ --- from 4

7. $d∈c⟺(d∈a ∧ ϕ(d))$ --- from 5

8. $d∈c ⟺ d∈b$ --- from 6 and 7

9. $∀z (z∈c⟺z∈b)$ --- from 8 by universal generalization

10. $c=b$ --- from 9 by extensionality

11. $∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b] \to (c=b)$ --- from 4a and 10 by Deduction Th, discharging premises 4a

12. $\lnot ∃y[∀z(z∈y⟺(z∈a∧ϕ(z))) ∧ y≠b]$ --- from 5c and 11 and taut: $(p \to \lnot q) \to [(p \to q) \to \lnot p]$ (ex falso)

13. $∀y[∀z(z∈y⟺(z∈a∧ϕ(z))) \to y=b]$ --- from 12 by equivalence for quantifiers and taut: $\lnot (p \land \lnot q) \Leftrightarrow (p \to q)$