Natural Deduction Problem: Predicate Logic with Identity in a Gentzen-style system

Question

I'm looking for a solution to this problem:

$$\left\{\forall x (Qx \leftrightarrow (\exists y (Rxy \wedge \neg x = y))),\quad \forall x Qx,\quad \exists x \exists y \forall z (z = x \vee z = y)\right\} \models \forall x \forall y (Rxy \leftrightarrow Ryx)$$

I can see that the brunt of the proof will come from making a contradiction between the identities in the conjunction and those in the first premise, but I'm not sure. Some help would be much appreciated!

Answer 1

01. ∀x[Qx↔[∃y[[Rxy]∧¬[x=y]]]] premise
02. ∀xQx                      premise
03. ∃x∃y∀z[[z=x]∨[z=y]]       premise
   04. ∃y∀z[[z=a]∨[z=y]]        assumption
      05. ∀z[[z=a]∨[z=b]]         assumption
         06. Rcd                    assumption
            07. ¬[c=d]                assumption
            08. ∀x[Qx↔[∃y[[Rxy]∧¬[x=y]]]] restate 01
            09. Qd↔[∃y[[Rdy]∧¬[d=y]]] ∀elim 08
            10. ∀xQx                  restate 02
            11. Qd                    ∀elim 10
            12. ∃y[[Rdy]∧¬[d=y]]      ↔elim 09 11
               13. [Rde]∧¬[d=e]         assumption
                  14. e=c                 assumption
                  15. [Rde]∧¬[d=e]        restate 13
                  16. [Rdc]∧¬[d=c]        para 15 14
                  17. Rdc                 ∧elim 16
               18. [e=c]→[Rdc]          →intro 19 17
                  19. ¬[e=c]              assumption
                  20. ∀z[[z=a]∨[z=b]]     restate 05
                  21. [c=a]∨[c=b]         ∀elim 20
                  22. [d=a]∨[d=b]         ∀elim 20
                  23. [e=a]∨[e=b]         ∀elim 20
                  24. [Rde]∧¬[d=e]        restate 13
                  25. ¬[d=e]              ∧elim 24
                     26. e=a                assumption
                     27. ¬[d=e]             restate 25
                     28. ¬[d=a]             para 27 26
                     29. [d=a]∨[d=b]        restate 22
                     30. d=b                ∨elim 29 28
                     31. ¬[e=c]             restate 19
                     32. ¬[a=c]             para 31 26
                     33. ¬[c=a]             flip 32
                     34. [c=a]∨[c=b]        restate 21
                     35. c=b                ∨elim 34 33
                     36. ¬[c=d]             restate 07
                     37. c=d                para 35 30
                     38. ⊥                  36 37
                  39. ¬[e=a]              ¬intro 26 38
                  40. e=b                 ∨elim 23 39
                  41. ¬[d=e]              restate 25
                  42. ¬[d=b]              para 41 40
                  43. d=a                 ∨elim 22 42
                  44. ¬[c=d]              restate 07
                  45. ¬[c=a]              para 44 43
                  46. c=b                 ∨elim 21 45
                  47. e=c                 para 40 46
                  48. ⊥                   47 19
               49. ¬¬[e=c]              ¬intro 19 48
               50. e=c                  ¬¬elim 49
               51. Rdc                  MP 18 50
            52. Rdc                   ∃ 12 13-51
         53. ¬[c=d]→[Rdc]           →intro 07 52
            54. c=d                   assumption
            55. Rcd                   restate 06
            56. Rcc                   para 55 54
            57. Rdc                   para 56 54
         58. [c=d]→[Rdc]            →intro 54 57
         59. [c=d]∨¬[c=d]           LEM
         60. Rdc                    ∨elim 58 53 59
      61. [Rcd]→[Rdc]             →intro 06 60
      62. ∀y[[Rcy]→[Ryc]]         ∀intro 61
      63. ∀x∀y[[Rxy]→[Ryx]]       ∀intro 62
   64. ∀x∀y[[Rxy]→[Ryx]]        ∃elim 04 05-63
65. ∀x∀y[[Rxy]→[Ryx]]         ∃elim 03 04-64
66. ∀y[[Ray]→[Rya]]           ∀elim 65
67. [Rab]→[Rba]               ∀elim 66
68. ∀y[[Rby]→[Ryb]]           ∀elim 65
69. [Rba]→[Rab]               ∀elim 68
70. [Rab]↔[Rba]               ↔intro 67 69
71. ∀y[[Ray]↔[Rya]]           ∀intro 70
72. ∀x∀y[[Rxy]↔[Ryx]]         ∀intro 71

Synopsis of proof:

We let $Rcd$. Then, using the premise $\forall x \exists y [Rxy \land \neg x = y]$, we conclude $Rde$. Then, we argue that $e$ must be equal to $c$, using $\forall z[z = a \lor z = b]$. Then, we conclude that $Rcd \implies Rdc$. Using symmetry, we conclude that $Rdc \implies Rcd$, hence $Rcd \iff Rdc$. Then, we generalize to $\forall x \forall y[Rxy \iff Ryx]$.