Some notation first. Let $E_X$ be the equivalence relation that you can obtain from a partition $X$, that is $\{p:\exists x\exists y\exists z(p=\langle x,y\rangle,z\in X,x\in z,y\in z)\}$. Instead, let $\text{dom}(\mathord{\sim})/\mathord{\sim}$ be the partition that you can obtain from an equivalence $\mathord{\sim}$.
I'd like to prove that if $X$ is a partition, then $\text{dom}(E_X)/E_X=X$.
My strategy is to prove separately that:
- $\text{dom}(E_X)/E_X\subseteq X$
- $X\subseteq\text{dom}(E_X)/E_X$.
This is what I managed to prove so far.
- Suppose $c\in\text{dom}(E_X)/E_X$. Then $\exists x(x\in\text{dom}(E_X),c=[x]_{E_X})$. Suppose $a\in\text{dom}(E_X),c=[a]_{E_X}$. Then $[a]_{E_X}\in\text{dom}(E_X)/E_X$. Then $a\in[a]_{E_X}$. Then $a\in c$. Then?
- Suppose $c\in X$. Then $c\not=\emptyset$. Then $\exists z(z\in c)$. Suppose $a\in c$. Then $\langle a,a\rangle\in E_X$. Then $a\in\text{dom}(E_X)$. Then $a\in[a]_{E_X}$. Then $[a]_{E_X}\in\text{dom}(E_X)/E_X$. Then $a\in\bigcup\text{dom}(E_X)/E_X$. Then?
Thanks.