Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima

In the setting of Sets and Maps: Ordinary Notation, with predicative meant for formulas with abbreviations, let $p$ be a set with a partial order $\preceq$, suprema and infima of subsets of $p$ being formed in $p$: bounds, suprema and infima are those of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order with $p$ for its $a$ and $\preceq$ for its $\le$. The letters $S$, $z$, $z'$, $b$ and $v$ are distinct set variables, the other letters parameters.

¶ Let $\sigma(S,z)$ be the formula

$$\forall v\,(v\in S\Rightarrow v\in p)\wedge z\in p\wedge\forall v\,(v\in S\Rightarrow v\preceq z)\wedge\forall b\,((b\in p\wedge\forall v\,(v\in S\Rightarrow v\preceq b))\Rightarrow z\preceq b),$$

and $\iota(S,z)$ the formula obtained by replacing $v\preceq z$, $v\preceq b$ and $z\preceq b$ in it by $z\preceq v$, $b\preceq v$ and $b\preceq z$. Both are predicative, and for sets $S$ and $z$: $\sigma(S,z)$ holds if and only if $S$ is a subset of $p$ that has a supremum and $z=\sup S$; $\iota(S,z)$ holds if and only if $S$ is a subset of $p$ that has an infimum and $z=\inf S$.

¶ Let $\gamma_{\sigma}(S)$ be the formula $(\exists z\,\sigma(S,z))\wedge\forall z\,\forall z'\,((\sigma(S,z)\wedge\sigma(S,z'))\Rightarrow z=z')$, where $\sigma(S,z')$ is $\sigma(S,z)$ with $z'$ put for $z$, and let $\gamma_{\iota}(S)$ be formed likewise from $\iota$. Then $\sigma(S,z)$, $\iota(S,z)$, $\gamma_{\sigma}(S)$ and $\gamma_{\iota}(S)$ are predicative, and for all values of the parameters and every set $S$ satisfying $\gamma_{\sigma}(S)$, respectively $\gamma_{\iota}(S)$, exactly one set $z$ satisfies $\sigma(S,z)$, respectively $\iota(S,z)$. As $\preceq$ is a partial order on $p$, $\gamma_{\sigma}(S)$ holds if and only if $S$ is a subset of $p$ that has a supremum, and then that set $z$ is $\sup S$; and $\gamma_{\iota}(S)$ holds if and only if $S$ is a subset of $p$ that has an infimum, and then that set $z$ is $\inf S$. So $\sup S$ and $\inf S$ are defined set symbols with argument $S$ given by $\sigma$ and $\iota$, used properly where $S\subseteq p$ has a supremum, respectively an infimum, and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination applies to them with $\sigma$ or $\iota$ as its $\theta$ and $\gamma_{\sigma}$ or $\gamma_{\iota}$ as its $\gamma$.

¶ For a set $a$ and an expression $t(u)$ as in Maps and Relations Given by Formulas §map that is a subset of $p$ with a supremum, respectively an infimum, for every $u\in a$, exactly one map $f:a\to p$ has $f(u)=\sup t(u)$, respectively $f(u)=\inf t(u)$, for every $u\in a$.