Proof of The Distance on the Real Numbers Is a Map with Values the Absolute Differences

Each result cited is universally quantified over the data in its own statement.

The clause map. By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field, and $\mathbb{R}$ is a set by The Real Numbers §reals. We apply Maps and Relations Given by Formulas §binary with the set $\mathbb{R}$ for each of $b$, $c$ and $d$ and with the expression $|s-t|$, written $e(v,w)$ for the expression of that clause to keep it apart from the variable $t$, so that $e(s,t)=|s-t|$. Both of its hypotheses hold. (i) For all $s,t\in\mathbb{R}$, the difference $s-t$ lies in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative, so $e(s,t)=|s-t|\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value; this is the hypothesis that $e(v,w)\in b$ for all $v\in c$ and $w\in d$. (ii) The defined set symbols of $|s-t|$ are used properly at the arguments $s,t\in\mathbb{R}$: there $s-t$ and $|s-t|$ are elements of $\mathbb{R}$ by (i), uniquely determined by Negatives, Differences, Reciprocals and Quotients §negative and Additive and Multiplicative Inverses Are Unique §negative for the negative and the difference and by Absolute Value in an Ordered Field §absolute-value for the absolute value; and the condition $s\in\mathbb{R}\wedge t\in\mathbb{R}\wedge z=|s-t|$ that this hypothesis concerns is given by a predicative formula, since by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §distance-formula, with $s$, $t$ and $z$ for its set variables $x$, $y$ and $z$ and with the ordered field $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ of the setting as the values of its variables $t_{1},\dots,t_{6}$, it is equivalent under every assignment to a predicative formula. So Maps and Relations Given by Formulas §binary gives exactly one map $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with $f((s,t))=e(s,t)=|s-t|$ for all $s,t\in\mathbb{R}$, that is, with $f(s,t)=|s-t|$, since $f(s,t)$ stands for $f((s,t))$ by Sets and Maps: Ordinary Notation §maps. By The Distance on the Real Numbers §distance, $d_{\mathbb{R}}$ is a map $\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with $d_{\mathbb{R}}(s,t)=|s-t|$ for all $s,t\in\mathbb{R}$, so by this uniqueness it is $f$. Moreover $d_{\mathbb{R}}$ is a set: $\mathbb{R}\times\mathbb{R}$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set, so by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members the map $d_{\mathbb{R}}$ is an element of the class of functions from $\mathbb{R}\times\mathbb{R}$ to $\mathbb{R}$, and an element of a class is a set by Classes, Membership, Sets and Proper Classes §set. This proves the clause map.

The clause values. By the clause map and Binary Operations on a Set §operation, $d_{\mathbb{R}}$ is a binary operation on the set $\mathbb{R}$, and by Binary Operations on a Set §notation its value at $s,t\in\mathbb{R}$ is $d_{\mathbb{R}}((s,t))=|s-t|$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation, applied to the set $\mathbb{R}$ and the binary operation $d_{\mathbb{R}}$, for all sets $s$, $t$ and $z$: $((s,t),z)\in d_{\mathbb{R}}$ if and only if $s\in\mathbb{R}$, $t\in\mathbb{R}$ and $z=d_{\mathbb{R}}((s,t))$, that is, by the clause map, if and only if $s\in\mathbb{R}$, $t\in\mathbb{R}$ and $z=|s-t|$.