So I am writing a paper on logic and set theory and need to prove that Kuratowski's definition of ordered pairs satisfies the biconditional. I know there have been many answers on this but I am trying to do a two column proof of this starting with the pair set axiom and arriving at the two instantiated sets {{a},{a,b}} and {{c},{c,d}}.
From that point it will be two direct proofs where the first assumption will be {{a},{a,b}}={{c},{c,d}}. However, since the axiom of extensionality only goes in one direction, I will have to refer to the substitution property of equality to proceed from this point.
(i) The part of the proof that is supposed to conclude with {a,a}={a} starts with the pair set axiom and then the axiom of extensionality, however, from the point where we state extentionality, we eventually instantiate {a}. To me this seems like we are presupposing {a} is a set in order to show that it is equal to {a,a}. Is this true? Is this the only way to prove the existence of singleton sets? Consider line 3.
- $\forall x\forall y(\forall u[u\in x\leftrightarrow u\in y]\rightarrow x=y)$ Extentionality
- $\forall y(\forall u[u\in\{a,a\}\leftrightarrow u\in y]\rightarrow \{a,a\}=y)$ 1 UI
- $\forall u[u\in\{a,a\}\leftrightarrow u\in\{a\}]\rightarrow x=y$ 2 UI
(ii) My second question is that when referring to the substituition property of equality, what are the abbreviations for these justifications? Would I just put "Sub" in the right hand column?