Proof of The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist

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

Sets and the data of $\mathbb{Z}$. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $\mathbb{N}$ is a set and $1\in\mathbb{N}$; $\mathbb{Z}$ is a set by The Integers §integers; so $Q=\mathbb{Z}\times\mathbb{N}$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. By The Cartesian Product of Two Classes §product and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, every element of $Q$ is $(x,m)$ for some $x\in\mathbb{Z}$ and $m\in\mathbb{N}$, and $(x,m)\in Q$ for all such $x$ and $m$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. By The Integers §embedding, $\iota:\mathbb{N}\to\mathbb{Z}$ is a map, so $\iota(n)\in\mathbb{Z}$ for $n\in\mathbb{N}$, and $(n,\iota(n))\in\iota$ by Functions, Values of a Function, and Functions from One Class to Another §value. Let $P$ denote the product of $\mathbb{Z}$ as a class, so that $xw=P((x,w))$ for $x,w\in\mathbb{Z}$; by The Integers §operations, The Integers §integers and Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order §operations, $P$ is a binary operation on $\mathbb{Z}$, and $xw\in\mathbb{Z}$ for $x,w\in\mathbb{Z}$ by Binary Operations on a Set §notation.

Clause approximation. Let $\varphi(u,v)$ be the formula

$$\exists x\,\exists m\,\exists y\,\exists n\,\exists z_{1}\,\exists z_{2}\,\exists z_{3}\,\bigl(x\in\mathbb{Z}\wedge m\in\mathbb{N}\wedge y\in\mathbb{Z}\wedge n\in\mathbb{N}\wedge u=(x,m)\wedge v=(y,n)\wedge(n,z_{1})\in\iota\wedge(m,z_{2})\in\iota\wedge((x,z_{1}),z_{3})\in P\wedge((y,z_{2}),z_{3})\in P\bigr),$$

with the parameters $\mathbb{Z}$, $\mathbb{N}$, $\iota$ and $P$. Its atomic parts with ordered pairs are predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-equality, Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §operation-membership; its only defined set symbol is the ordered pair, applied to set variables, so it is used properly, the ordered pair of two sets being a set by The Ordered Pair of Two Sets and Nested Tuples §pair; and all its quantifiers bind set variables. So $\varphi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, and it meets the hypotheses of Maps and Relations Given by Formulas §relation.

We show that for all $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, $\varphi((x,m),(y,n))$ holds if and only if $x\,\iota(n)=y\,\iota(m)$. The defined set symbols $\iota(n)$, $\iota(m)$, $x\,\iota(n)$ and $y\,\iota(m)$ are each used properly here, by the first paragraph; explicitly: suppose $\varphi((x,m),(y,n))$ holds with witnesses $x',m',y',n',z_{1},z_{2},z_{3}$. Then $(x,m)=(x',m')$ and $(y,n)=(y',n')$, so $x=x'$, $m=m'$, $y=y'$ and $n=n'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value, applied to the function $\iota$, $z_{1}=\iota(n)$ and $z_{2}=\iota(m)$, which lie in $\mathbb{Z}$; then by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §operation, applied to $P$ on $\mathbb{Z}$, $z_{3}=x\,\iota(n)$ and $z_{3}=y\,\iota(m)$, so $x\,\iota(n)=y\,\iota(m)$. Conversely, if $x\,\iota(n)=y\,\iota(m)$, the sets $x,m,y,n$, $z_{1}=\iota(n)$, $z_{2}=\iota(m)$ and $z_{3}=x\,\iota(n)$ witness $\varphi((x,m),(y,n))$, by the same two clauses.

By Maps and Relations Given by Formulas §relation, applied to the set $Q$ and the formula $\varphi$, there is exactly one relation $R_{0}$ on $Q$ with $(u,v)\in R_{0}$ if and only if $\varphi(u,v)$, for all $u,v\in Q$. Since $(x,m),(y,n)\in Q$ for $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$, the previous paragraph shows that $R_{0}$ has the property of the clause. If $R$ is any relation on $Q$ with that property, let $u,v\in Q$ and write $u=(x,m)$ and $v=(y,n)$ with $x,y\in\mathbb{Z}$ and $m,n\in\mathbb{N}$; then $(u,v)\in R$ if and only if $x\,\iota(n)=y\,\iota(m)$, that is, if and only if $\varphi(u,v)$. So $R=R_{0}$ by the uniqueness in Maps and Relations Given by Formulas §relation. Hence exactly one relation on $Q$ has the property of the clause. The relation $\approx$ of Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §equivalence is, by the statement of that lemma, the relation on $Q$ with this property; so $\approx$ is $R_{0}$.

Clause operations. By the clause approximation, $\approx$ is the relation on $Q$ that Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order is stated for, so its clauses apply to it; and $\mathbb{Q}=Q/{\approx}$ by The Rational Numbers §rationals. By Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §operations, there are unique binary operations on $\mathbb{Q}$, a unique map from $\mathbb{Q}$ to $\mathbb{Q}$ and a unique relation on $\mathbb{Q}$ with the values displayed in the clause; by The Rational Numbers §operations, the sum $+$, the product $\cdot$, the negation $-$ and the order $\le$ on $\mathbb{Q}$ are these. This is the clause.

Clause embedding. We apply Maps and Relations Given by Formulas §map to the sets $\mathbb{Z}$ and $\mathbb{Q}$, the latter a set by The Rational Numbers §rationals, and to the expression $t(u)=[u,1]$. For $u\in\mathbb{Z}$, the pair $(u,1)$ is a set by The Ordered Pair of Two Sets and Nested Tuples §pair and lies in $Q$, as $1\in\mathbb{N}$; and $\approx$ is an equivalence relation on the set $Q$ by Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §equivalence, which applies by the clause approximation. So, by The Equivalence Class of an Element under an Equivalence Relation §class, $[u,1]$ is a set and a defined set symbol, used properly for every $u\in\mathbb{Z}$. Finally, $[u,1]\in Q/{\approx}=\mathbb{Q}$ for every $u\in\mathbb{Z}$ by Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order §equal. Hence Maps and Relations Given by Formulas §map gives exactly one map $f$ from $\mathbb{Z}$ to $\mathbb{Q}$ with $f(u)=[u,1]$ for every $u\in\mathbb{Z}$. By The Rational Numbers §embedding, $j$ is the map from $\mathbb{Z}$ to $\mathbb{Q}$ with $j(x)=[x,1]$ given by Maps and Relations Given by Formulas §map, that is, $j=f$. This is the clause.