Prove reflexivity using Fitch software

Question

I am trying to learn how to use the Fitch software from Barwise and Etchemendy to develop proofs. I am trying to prove that $R$ is reflexive from the following premises.

If $R$ is symmetric, transitive, and if $R$ relates $x$ to some element in the domain, then it relates $x$ to itself. Which I have formalised (perhaps incorrectly) as:

In the proof above, I have used First Order consequence (FO Con) which does not help me understand the proof itself. I would like to represent the proof in Fitch without using FO Con. Here is my best effort:

Any help in completing this proof would be appreciated.

I have migrated this question from Computer Science Stack Exchange.

Answer 1

First of all, to prove a universal you need to unievrsal proof structure, i.e. set up a $\forall$ Intro by starting a subproof with $a$ as an arbitrary object. Here is the basic set-up you therefore need:

Then inside this subproof you can get the all important existential, and do another subproof of the kind you already have to eliminate this existential, but make sure to introduce a $b$ as the witness for that existential:

The rest is pretty much as you had it.