The Extended Real Line, Its Order, and [0,∞]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $\mathbb{R}$ and its order $\le$ be as in The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii); $\mathbb{R}$ is a set by The Real Numbers (i).

(i) Let $\infty=\mathbb{R}$ and $-\infty=\{\mathbb{R}\}$, the singleton of $\mathbb{R}$. Then $\infty\notin\mathbb{R}$, $-\infty\notin\mathbb{R}$ and $-\infty\neq\infty$, by No Set Is an Element of Itself, Nor Is Its Singleton, and No Set Equals Its Singleton (i), No Set Is an Element of Itself, Nor Is Its Singleton, and No Set Equals Its Singleton (ii) and No Set Is an Element of Itself, Nor Is Its Singleton, and No Set Equals Its Singleton (iii), applied to the set $\mathbb{R}$.

(ii) The extended real line is the set $[-\infty,\infty]=\mathbb{R}\cup\{-\infty,\infty\}$, with $\{-\infty,\infty\}$ the unordered pair of the sets $-\infty$ and $\infty$, and $[0,\infty]=\{x\in\mathbb{R}:0\le x\}\cup\{\infty\}$; both are sets, as unions of sets. Thus $x\in[-\infty,\infty]$ if and only if $x\in\mathbb{R}$ or $x=-\infty$ or $x=\infty$; $x\in[0,\infty]$ if and only if either $x\in\mathbb{R}$ and $0\le x$, or $x=\infty$; and $[0,\infty]\subseteq[-\infty,\infty]$.

(iii) For $x,y\in[-\infty,\infty]$, $x\le y$ means that $x,y\in\mathbb{R}$ and $x\le y$ in $\mathbb{R}$, or $x=-\infty$, or $y=\infty$; this relation is the set $\{p\in[-\infty,\infty]\times[-\infty,\infty]:(p_{1},p_{2}\in\mathbb{R}\wedge p_{1}\le p_{2})\vee p_{1}=-\infty\vee p_{2}=\infty\}$, with $p=(p_{1},p_{2})$ given by its components. Further, $x<y$ means $x\le y$ and $x\neq y$; $x\ge y$ means $y\le x$, and $x>y$ means $y<x$. For $x,y\in\mathbb{R}$, neither $x=-\infty$ nor $y=\infty$ holds, by (i), so $x\le y$ holds if and only if $x\le y$ in $\mathbb{R}$; this is why the symbols of $\mathbb{R}$ are used.