Predicative Formulas for Bijections from a Segment [n] and for Increasing Listings

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, with predicative meant for formulas with abbreviations, conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); (i) and (ii) are statements of the metatheory. For $n\in\mathbb{N}_{0}$, $[n]$ is as in Intervals of Natural Numbers (ii); bijections are as in Injective, Surjective and Bijective Functions between Classes (iii), and $x(i)$ is the value of a map $x$ at a point $i$ of its domain. The letters $f$, $x$, $n$ and $B$ are distinct set variables, and $\mathbb{N}_{0}$, $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the strict order $<$ of $\mathbb{R}$ are parameters. For $i,j\in\mathbb{N}_{0}$, $i<j$ refers to the strict order of $\mathbb{N}_{0}$, as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (v); and $x(i)<x(j)$ means that the ordered pair $(x(i),x(j))$ lies in the strict order $<$ of $\mathbb{R}$.

(i) The condition "$n\in\mathbb{N}_{0}$ and $f$ is a bijection from $[n]$ onto $B$" on $f$, $n$ and $B$ is expressed by a predicative formula.

(ii) The condition "$n\in\mathbb{N}_{0}$, $x$ is a bijection from $[n]$ onto $B$, and $x(i)<x(j)$ for all $i,j\in[n]$ with $i<j$" on $x$, $n$ and $B$ is expressed by a predicative formula.