Predicate logic inference in a simple proof of uniform continuity. For a function $f$ from a metric space $X$ into a metric space $Y$, uniform continuity can defined in this way:
$\forall ε>0:\existsδ > 0:\forall p,q\in X:d_{X}(p,q)<δ \rightarrow d_{Y}(f(p),f(q))<ε   $
I want to prove this is equivalent to:
$\forall ε>0:\existsδ > 0:\forall E\subset X:diam\,E<δ \rightarrow diam\,f(E)<ε   $
I have some inference gaps in my reasoning. I will go step by step because I'm new to proving using predicate logic. The outline of the proof ($\rightarrow$ only) is the following:


*

*Fix $ε$, and for $\frac{ε}{2}$ I get the corresponding $δ$.

*Take any $E\subset X$, such that $diam\,E<δ$.

*If $diam\,E<δ$ then $\forall p,q\in E:d_{X}(p,q)\leq diam\,E<δ$

*Since $\forall p,q\in X:d_{X}(p,q)<δ \rightarrow d_{Y}(f(p),f(q))<\frac{ε}{2}$

*Then $\forall p,q\in E:d_{X}(p,q)<δ \rightarrow d_{Y}(f(p),f(q))<\frac{ε}{2}$

*Then $diam\,f(E)\leq \frac{ε}{2}<ε$

*Since $E$ was arbitrary, we can generalize $\forall E\subset X$


I don't see how to connect steps 5 and 6. I want to know whether there is a specific inference rule for those steps.
 A: I find doing proofs this way (especially in analysis) very helpful in understanding the details of what is happening. Here is a complete proof for the forward direction; of course I would shorten in considerably if I were to tun it in as an assignment or just thinking through it for myself.


*

*$f: (X, d) \rightarrow (Y, \rho)$ is uniformly continuous

*$E \subset X$ 

*$\forall \varepsilon > 0 \, \exists \delta > 0 \, \forall x, y, \in X \,(d(x, y) < \delta\implies \rho(f(x), f(y))< \varepsilon)$ (by definition).

*$\exists \delta > 0 \, \forall x, y, \in X \,(d(x, y) < \delta\implies \rho(f(x), f(y))< \frac{\varepsilon}{2})$ (by universal instantation)

*$\forall x, y, \in X \,(d(x, y) < \delta\implies \rho(f(x), f(y))< \frac{\varepsilon}{2})$ (by existential instantation)

*$\forall x, y, \in E \,(d(x, y) < \delta\implies \rho(f(x), f(y))< \frac{\varepsilon}{2})$ (by 2)

*$d(x, y) < \delta\implies \rho(f(x), f(y))< \frac{\varepsilon}{2}$ (by universal instantation)

*$diam(E) = \sup \{d(x, y) : x, y\in E\}$ (defenition)

*$diam(E) < \delta$ (begin conditional proof)

*$d(x, y) \leq \sup \{d(x, y) : x, y\in E\}$ (by defenition of supremum)

*$d(x, y) \leq diam(E)$ (by 8, 10)

*$d(x, y) <\delta$ (by 9, 11)

*$\rho(f(x), f(y)) < \frac{\varepsilon}{2}$ (by 7 and 12)

*$\forall x, y \in E (\rho(f(x), f(y)) < \frac{\varepsilon}{2})$ (by universal generalization)

*$\forall f(x), f(y) \in f(E)\, ( \rho(f(x), f(y)) < \frac{\varepsilon}{2})$

*$\frac{\varepsilon}{2}$ is an upper bound for $\{\rho(f(x), f(y)) : f(x), f(y)\in f(E)\}$ (by defenition of upper bound)

*$\sup \{\rho(f(x), f(y)) : f(x), f(y)\in f(E)\} \leq \frac{\varepsilon}{2}$ (by defenition of supremum)

*$\frac{\varepsilon}{2} < \varepsilon$

*$\sup \{\rho(f(x), f(y)) : f(x), f(y)\in f(E)\} < \varepsilon$ (by 17 and 18)

*$diam(f(E)) <\varepsilon$ (by 8, 19)

*$diam(E)<\delta \implies diam(f(E))<\varepsilon$ (9 -20 conditional proof)

*$ \forall E \subset X \, (diam(E)<\delta \implies diam(f(E))<\varepsilon)$ (by universal generalization)

*$\exists \delta > 0 \,\forall E \subset X \, (diam(E)<\delta \implies diam(f(E))<\varepsilon)$ (by exestential generalization)

*$\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall E \subset X \;(diam(E)<\delta \implies diam(f(E))<\varepsilon)$ (by universal generalization)
A: There's more than logical inference to be done in this step.  I think that, in effect, you need the following lemma:

For all real numbers $r$, if for every $p,q \in E$ we have $d(p,q) \le r$, then $\operatorname{diam}(E) \le r$.

The proof of this lemma essentially involves looking at the definition of $\operatorname{diam}(E)$, which is defined as a certain supremum, and unwinding the definition of "supremum".
