Proof of $\mathbb{R}^1$ with the Euclidean Distance Is Isometric to the Real Line

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

The rules of arithmetic and order in the ordered field $\mathbb{R}$, carried by Commutative Rings, Fields and Ordered Fields: Standard Notation §ordered-fields, are used without further citation.

The index set. By Intervals of Natural Numbers §segment and Intervals of Natural Numbers §interval, $[1]=\{k\in\mathbb{N}_{0}:1\le k\le1\}$. The order of $\mathbb{N}_{0}$ is a well-order by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, hence a total order by Well-Orders on a Set §well-order, and so, by Partial and Total Orders on a Set and the Associated Strict Relation §total and Partial and Total Orders on a Set and the Associated Strict Relation §partial, a partial order, which is reflexive and antisymmetric. So $1\in[1]$ and every $k\in[1]$ equals $1$: $[1]=\{1\}$. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, the elements of $\mathbb{R}^{1}$ are the maps $[1]\to\mathbb{R}$, and $x_{1}=x(1)$ for $x\in\mathbb{R}^{1}$.

The maps. For $x\in\mathbb{R}^{1}$, $x_{1}\in\mathbb{R}$, so $\pi:\mathbb{R}^{1}\to\mathbb{R}$, $x\mapsto x_{1}$, is a map by Sets and Maps: Ordinary Notation §maps, the condition $z=x_{1}$ being predicative 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 §value-substitution. For $s\in\mathbb{R}$, let $(s)$ be the constant map $[1]\to\mathbb{R}$ with value $s$ of Pointwise Operations on Real-Valued Maps §constants (with $I=[1]$); it lies in $\mathbb{R}^{1}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, its only component is $(s)_{1}=s$, and so it is the $1$-tuple written $(s)$ in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. Thus $\sigma:\mathbb{R}\to\mathbb{R}^{1}$, $s\mapsto(s)$, is a map by Sets and Maps: Ordinary Notation §maps.

For $s\in\mathbb{R}$, $(\pi\circ\sigma)(s)=\pi((s))=(s)_{1}=s=\mathrm{id}_{\mathbb{R}}(s)$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §identity. For $x\in\mathbb{R}^{1}$, $(\sigma\circ\pi)(x)=(x_{1})$ is an element of $\mathbb{R}^{1}$ whose component at $1$, the only element of $[1]$, is $x_{1}$; so $(\sigma\circ\pi)(x)=x=\mathrm{id}_{\mathbb{R}^{1}}(x)$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality. The maps $\pi\circ\sigma$ and $\mathrm{id}_{\mathbb{R}}$ have the same domain $\mathbb{R}$ and the same values, and likewise $\sigma\circ\pi$ and $\mathrm{id}_{\mathbb{R}^{1}}$ on $\mathbb{R}^{1}$, so $\pi\circ\sigma=\mathrm{id}_{\mathbb{R}}$ and $\sigma\circ\pi=\mathrm{id}_{\mathbb{R}^{1}}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion, $\pi$ is bijective and $\pi^{-1}=\sigma$, that is, the inverse of $\pi$ maps $s\in\mathbb{R}$ to the $1$-tuple $(s)$.

The distance. Let $x,y\in\mathbb{R}^{1}$ and $a=x_{1}-y_{1}$, a real number by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative. By Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance, Sums and Products over a Finite Set and over an Interval §intervals (which identifies $\sum_{k=1}^{1}$ with the iterated sum of Iterated Operations: Finite Sums and Finite Products §iterated) and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion,

$$d_{E}(x,y)^{2}=\sum_{k=1}^{1}(x_{k}-y_{k})^{2}=a^{2}.$$

Also $d_{E}(x,y)=\lVert x-y\rVert\ge0$ by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §distance and Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square §square, and $|a|\ge0$ with $|a|^{2}=|a^{2}|=a^{2}$, by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §sign and Absolute Value in an Ordered Field §absolute-value, as $a^{2}=a\,a\ge0$ (here $a^{2}=a\,a$ by Arithmetic and Order of the Natural Numbers §digits, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product). Since $d_{E}(x,y)^{2}=|a|^{2}$ with both bases nonnegative (and $|a|\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value), Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff (exponent $2\ge1$) gives $d_{E}(x,y)=|a|$. Finally, by The Distance on the Real Numbers §distance and The Distance on the Real Numbers Is a Map with Values the Absolute Differences §map,

$$d_{\mathbb{R}}(\pi(x),\pi(y))=|x_{1}-y_{1}|=|a|=d_{E}(x,y).$$