Upper Bounds of Elements of [0,∞], and the Graph of a Section of a Map on ℕ×X

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $[-\infty,\infty]$, $[0,\infty]$ and the order $\le$ of $[-\infty,\infty]$ be as in The Extended Real Line, Its Order, and [0,∞] (ii) and The Extended Real Line, Its Order, and [0,∞] (iii). For a map $F$, $F(u)$ is its value at $u$; $(u,v)$ is the ordered pair, $\mathbb{N}\times X$ the Cartesian product, and $w(n,y)$ stands for $w((n,y))$.

(i) Let $C$ be a class and let $s\in[-\infty,\infty]$ satisfy $c\le s$ for every $c\in C$ and $s\le t$ for every $t\in[-\infty,\infty]$ with $c\le t$ for all $c\in C$. If some element of $C$ lies in $[0,\infty]$, then $s\in[0,\infty]$.

(ii) Let $X$ be a class, let $w:\mathbb{N}\times X\to[0,\infty]$ and $g:X\to[0,\infty]$ be maps, and let $n\in\mathbb{N}$ with

$$g(y)=w(n,y)\quad\text{for every }y\in X.$$

Then $((n,y),v)\in w$ for every $y\in X$ and every set $v$ with $(y,v)\in g$.