Shortest FOL deduction for $\forall x \forall y(x = y \to y = x)$ In Enderton's A Mathematical Introduction to Logic (second edition, SECTION 2.4 - A Deductive Calculus, page 122), he provides a worked example shown below. 

Show that $\vdash\forall x\forall y(x=y\to y=x)$:
  
  
*
  
*$\vdash x=y\to (x=x\to y=x)\qquad\text{(Axiom 6)}$
  
*$\vdash x=x\qquad\qquad\qquad\qquad\qquad\quad\text{(Axiom 5)}$
  
*$\vdash x=y\to y=x\qquad\qquad\qquad\quad\text{(Rule T)}$
  
*$\vdash \forall x\forall y(x=y\to y=x)\qquad\qquad\text{(Generalization Theorem applied twice)}$

After the worked example, he says:
"It must be emphasized that the four numbered lines above DO NOT
constitute a deduction of $\forall x \forall y(x = y \to y = x)$. Instead they form a proof (in the meta-language we continue, with little justification,
to call English) that such a deduction exists. The shortest deduction
of $\forall x \forall y(x = y \to y = x)$ known to the author is a sequence of
17 formulas."
My question is: Why does he say that this proof is in the meta-language? I would think that it is still a deduction in FOL with some intermediate steps left out (or few rules not fully expanded into the basic axioms)? Can you please help me in understanding what I am missing here?
For example, Expanding Rule T, we can rewrite the above as:

Show that $\vdash\forall x\forall y(x=y\to y=x)$:
  
  
*
  
*$\vdash x=y\to (x=x\to y=x)\qquad\text{(Axiom 6)}$
  
*$\vdash (x=y\to (x=x\to y=x)) \to (x=x \to (x=y \to y=x))\qquad\text{(Tautology: $(A \to (B \to C)) \to (B \to (A \to C))$ applied to 1)}$
  
*$\vdash x=x \to (x=y \to y=x)\qquad\text{(MP: From 1 and 2)}$
  
*$\vdash x=x\qquad\qquad\qquad\qquad\qquad\quad\text{(Axiom 5)}$
  
*$\vdash x=y\to y=x\qquad\qquad\qquad\quad\text{(MP: From 3 and 4)}$
  
*$\vdash \forall y(x=y\to y=x)\qquad\qquad\quad\text{(Generalization Theorem)}$
  
*$\vdash \forall x\forall y(x=y\to y=x)\qquad\qquad\text{(Generalization Theorem)}$

If we go further and write the generalization theorem in terms of the basic axioms, would that then constitute a proper deduction? If not, then what exactly are the 17 formulas that he mentions to be the shortest deduction in FOL?
Also, can you please give me hints on how to get to the '17 formulas deduction' for this problem? 

For reference, here are the axioms in the system that Enderton uses (modus ponens is the only rule of inference):
  
  
*
  
*Tautologies (wffs obtainable from tautologies of sentential
  logic having only the connectives $\neg$ and $\to$)
  
*$\forall x \alpha \to \alpha_t^x$ , where $t$ is substitutable for $x$ in $\alpha$
  
*$ \forall x( \alpha \to \beta)→( \forall x \alpha \to \forall x \beta)$
  
*$\alpha \to \forall x \alpha$, where x does not occur free in $\alpha$
  
*$x = x$
  
*$x = y \to (\alpha \to \alpha^1 )$, where $\alpha$ is atomic and $\alpha^1$ is obtained from $\alpha$ by replacing $x$ in zero or more (but not necessarily all) places by $y$.
  

 A: One of the reasons is that the Generalization Theorem [see page 117] used in the last step of the proof is not a rule of the calculus, but a so-called meta-theorem.
It is a theorem about $\vdash$, i.e. the derivability relation, and $\vdash$ is not part of the syntax of the calculus [see page 69].
The theorem asserts that (under certain circumstances) a derivation in the calculus exists, but it is not itself a derivation in the calculus.
We can convert the proof provided at page 122 into a "fully formal" derivation following the steps in the proof of the Gen Th, inserting the "missing" steps.
Example : how to remove the first use of Gen Th in step 4 ? We have to use the Case 3 of the proof of the meta-theorem.
In your expanded proof we have to use the universal closure of step 3) :

3a) $\forall x (x=x → (x=y → y=x))$

as well as that of Ax.5 :

4a) $\forall x (x=x).$

Thus :

4b) $\forall x (x=x → (x=y → y=x)) \to (\forall x (x=x) → \forall x (x=y → y=x))$ --- Ax.3
4c) $\forall x (x=x) → \forall x (x=y → y=x))$ --- from 3a) and 4b) by MP
4d) $\forall x (x=y → y=x)$ --- from 4a) and 4c) by MP.

The same procedure must then be used to derive 3a) above from Ax.6 and the universal closure of step 2 (see page 112 : "The logical axioms are then all generalizations of wffs of the following forms [...] : 1. Tautologies; [...]").
In the same way, for the 2nd use of Gen Th.

The same for Rule T [page 118] used in step 3: you have already provided the "elimination" of it inserting into the proof the corresponding elementary propositional steps.
