Proof of Integer and Rational Brackets as Typed Terms

Terms under $\gamma$, their values and terms of a type are as in Terms and Typed Terms under a Guard (i) and Terms and Typed Terms under a Guard (ii); throughout, the parameters have their fixed values, as in Conditions Expressed by a Predicative Formula, and Guards (i).

Proof of (i). $P$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), $\mathbb{N}$ being a set by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), and $\sim$ is an equivalence relation on $P$ by Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order (i). So by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (vi), $\pi_{\sim}$ is a map from $P$ to $P/{\sim}=\mathbb{Z}$ with $\pi_{\sim}(p)=[p]_{\sim}$, the equivalence class of $p$, for every $p\in P$. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), $(s,t)$ is a term of type $\mathbb{N}\times\mathbb{N}=P$ under $\gamma$, and by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), with $\pi_{\sim}$ for $F$, $\pi_{\sim}((s,t))$ is a term of type $\mathbb{Z}$ under $\gamma$. Its value, for values $a$ and $b$ of $s$ and $t$, is $[(a,b)]_{\sim}$, which is the class $[a,b]$ of Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order (i).

Proof of (ii). $\mathbb{Z}$ is a set by The Integers (i), so $Q$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), and $\approx$, which satisfies the condition of Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order (i) by The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist (i), is an equivalence relation on $Q$ by Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order (i). Here the relation $\approx$ of The Rational Numbers (i), from which $\mathbb{Q}=Q/{\approx}$ is formed, is the relation on $Q$ introduced in Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order, the one with $(x,m)\approx(y,n)$ if and only if $x\,\iota(n)=y\,\iota(m)$, with $\iota$ as in The Integers (v): by The Relation, Operations, Order and Embedding Defining the Rational Numbers Exist (i), it is the unique relation on $Q$ with this property. So by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection (vi), $\pi_{\approx}$ is a map from $Q$ to $Q/{\approx}=\mathbb{Q}$ with $\pi_{\approx}(p)=[p]_{\approx}$ for every $p\in Q$. By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), $(s,t)$ is a term of type $\mathbb{Z}\times\mathbb{N}=Q$ under $\gamma$, and by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), with $\pi_{\approx}$ for $F$, $\pi_{\approx}((s,t))$ is a term of type $\mathbb{Q}$ under $\gamma$, whose value, for values $x$ and $m$ of $s$ and $t$, is $[(x,m)]_{\approx}$, the class $[x,m]$ of Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order (i).