The Graph of Multiplication on ℕ₀ Is Given by a Predicative Formula

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $x_{0},x_{1},x_{2}$ be distinct set variables, let $\mathbb{N}_{0}$ be as in The Class Omega of Natural Numbers with Zero (i), for $m,n\in\mathbb{N}_{0}$ let $m\cdot n$ be their product, and let $(u,v)$ denote the ordered pair. Each clause asserts that the condition shown is expressed by a predicative formula, the variables it names being the $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i), with no displayed variables.

(i) The graph on three variables. The condition on $x_{0},x_{1},x_{2}$

$$x_{1}\in\mathbb{N}_{0},\quad x_{2}\in\mathbb{N}_{0}\quad\text{and}\quad x_{0}=((x_{1},x_{2}),x_{1}\cdot x_{2}).$$

(ii) The graph on one variable. The condition on $x_{0}$

$$\text{there are sets } m \text{ and } n \text{ with } m\in\mathbb{N}_{0},\ n\in\mathbb{N}_{0}\ \text{and}\ x_{0}=((m,n),m\cdot n).$$