Arithmetic on [0,∞]: Bookkeeping

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{R}$, its order $\le$, its sum, its product and its element $0$ be as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii), and let $[0,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (ii). Let $[0,\infty]\times[0,\infty]$ be the Cartesian product, $(u,v)$ the ordered pair of sets $u$ and $v$, and $p_{1},p_{2}$ the components of an ordered pair $p$.

(i) For every condition $\varphi$ on two classes and every set $p$, with $p_{1},p_{2}$ the components of $p$ (meaningful when $p$ is an ordered pair, in particular when $p$ lies in the product): $p\in[0,\infty]\times[0,\infty]$ and $\varphi(p_{1},p_{2})$ hold if and only if there are sets $u$ and $v$ with $u,v\in[0,\infty]$, $p=(u,v)$ and $\varphi(u,v)$.

(ii) If $x,y\in\mathbb{R}$, $0\le x$ and $0\le y$, then the sum $x+y$ formed in $\mathbb{R}$ lies in $[0,\infty]$.

(iii) If $x,y\in\mathbb{R}$, $0\le x$ and $0\le y$, then the product $xy$ formed in $\mathbb{R}$ lies in $[0,\infty]$.