|
|
$$\begin{array}{rlrl}
1&{_{\:\!\mathbf|}}~\forall xRxx\\[-5pt]
2&\big|~\forall x\forall y(Rxy\to Ryx\to x=y)\\[-5pt]
3&\big|\!\underline{\,~\forall x\forall y(Rxy\to Ryx)~}\\[-5pt]
4&\big|~\forall y(Ray\to Rya\to a=y)&\rm{{\forall}E}&\rm{2}\\[-5pt]
5&\big|~\forall y(Ray\to Rya)&\rm{{\forall}E}&\rm{3}\\[-5pt]
6&\big|~Rab\to Rba\to a=b&\rm{{\forall}E}&\rm{4}\\[-5pt]
7&\big|~Rab\to Rba&\rm{{\forall}E}&\rm{5}\\[-5pt]
8&\big|~{_{\:\!\mathbf|}}\!\underline{\,~Rab~}\\[-5pt]
9&\big|~\big|~Rba\to a=b&\rm{{\to}E}&\rm{6,8}\\[-5pt]
10&\big|~\big|~Rba&\rm{{\to}E}&\rm{7,8}\\[-5pt]
11&\big|~\big|~a=b&\rm{{\to}E}&\rm{9,10}\\[-5pt]
12&\big|~{_{\:\!\mathbf|}}\!\underline{\,~a=b~}\\[-5pt]
13&\big|~\big|~Raa&\rm{{\forall}E}&\rm{1}\\[-5pt]
14&\big|~\big|~Rab&\rm{{=}E}&\rm{12,13}\\[-5pt]
15&\big|~Rab\leftrightarrow a=b&\rm{{\leftrightarrow}I}&\rm{8{-}11,12{-}14}\\[-5pt]
16&\big|~\forall y(Ray\leftrightarrow a=y)&\rm{{\forall}I}&\rm{15}\\[-5pt]
17&\big|~\forall x\forall y(Rxy\leftrightarrow x=y)&\rm{{\forall}I}&\rm{16}\\[-5pt]
\end{array}$$
|
|
|