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

Each result cited is universally quantified over the data in its own statement.

Clause supremum. Predicativity. By Partial and Total Orders on a Set and the Associated Strict Relation §partial, $v\preceq z$, $v\preceq b$, $z\preceq b$ and the parts of $\iota$ replacing them stand for $(v,z)\in{\preceq}$ and the like, written with the ordered pair as a defined set symbol. The other atomic parts are memberships, the quantifiers are over the set variables $v$ and $b$, and no class abstraction is written in $\sigma$ or $\iota$. So no quantifier of $\sigma$ or $\iota$ is applied to a class variable, and both are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Meaning. Let $S$ and $z$ be sets. The first conjunct of $\sigma(S,z)$, which is also that of $\iota(S,z)$, holds if and only if $S\subseteq p$, by Subclasses and Subsets §subclass; if it fails, both sides of both claims fail. Let now $S$ be a subset of $p$. By Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §bounds, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, for every set $b$, $b\in\operatorname{Ub}(S)$ if and only if $b\in p$ and $v\preceq b$ for every $v\in S$, and $b\in\operatorname{Lb}(S)$ if and only if $b\in p$ and $b\preceq v$ for every $v\in S$. Hence the second and third conjuncts of $\sigma(S,z)$ state that $z\in\operatorname{Ub}(S)$, and the fourth that $z\preceq b$ for every $b\in\operatorname{Ub}(S)$; by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least, together they state that $z$ is a least element of $\operatorname{Ub}(S)$, that is, by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §supremum, a supremum of $S$. Likewise the second and third conjuncts of $\iota(S,z)$ state that $z\in\operatorname{Lb}(S)$, and the fourth that $b\preceq z$ for every $b\in\operatorname{Lb}(S)$; together they state that $z$ is a greatest element of $\operatorname{Lb}(S)$, that is, an infimum of $S$. Since $S$ has at most one supremum and at most one infimum, by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §supremum, $z$ is a supremum of $S$ if and only if $S$ has a supremum and $z=\sup S$, and $z$ is an infimum of $S$ if and only if $S$ has an infimum and $z=\inf S$.

Clause bound-symbol. We give the argument for $\sigma$; the one for $\iota$ is the same with $\iota$, infimum, $\inf S$ and $\operatorname{Lb}(S)$ in place of $\sigma$, supremum, $\sup S$ and $\operatorname{Ub}(S)$.

Predicativity. $\sigma(S,z)$ is predicative by the clause supremum. The formula $\sigma(S,z')$ is $\sigma(S,z)$ with the set variable $z'$, which does not occur in $\sigma$, put for $z$, so it has the same quantifiers as $\sigma$; and $\gamma_{\sigma}(S)$ is built from $\sigma(S,z)$, $\sigma(S,z')$ and the formula $z=z'$ by connectives and quantifiers over the set variables $z$ and $z'$. As no quantifier of $\sigma$ is applied to a class variable, neither is any quantifier of $\gamma_{\sigma}(S)$, and $\gamma_{\sigma}(S)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure.

Uniqueness. Fix any values of the parameters, and let $S$ be a set with $\gamma_{\sigma}(S)$. By its first conjunct some set $z$ satisfies $\sigma(S,z)$, and by its second any sets $z$ and $z'$ with $\sigma(S,z)$ and $\sigma(S,z')$ are equal. So exactly one set $z$ satisfies $\sigma(S,z)$.

The partial order $\preceq$. Let $S$ be a set. By the clause supremum, $\sigma(S,z)$ holds for a set $z$ if and only if $S$ is a subset of $p$ that has a supremum and $z=\sup S$. Hence the first conjunct of $\gamma_{\sigma}(S)$ holds if and only if $S$ is a subset of $p$ that has a supremum, and then any sets $z$ and $z'$ with $\sigma(S,z)$ and $\sigma(S,z')$ both equal $\sup S$, so the second conjunct holds as well. So $\gamma_{\sigma}(S)$ holds if and only if $S$ is a subset of $p$ that has a supremum, and then $\sup S$ is the set $z$ with $\sigma(S,z)$. For a subset $S$ of $p$, $\sigma(S,z)$ agrees with the formula $z\in\operatorname{Ub}(S)\wedge\forall b\,(b\in\operatorname{Ub}(S)\Rightarrow z\preceq b)$ of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §supremum, by the paragraph Meaning of the clause supremum; so the symbol given by $\sigma$ is the supremum of that definition.

The defined set symbol. By the above, $\sigma$ and $\gamma_{\sigma}$ are predicative and, for all values of the parameters and all sets $S$ satisfying $\gamma_{\sigma}(S)$, exactly one set $z$ satisfies $\sigma(S,z)$; these are the hypotheses of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination with $k=1$, $S$ for $v_{1}$, $\sigma$ for $\theta$ and $\gamma_{\sigma}$ for $\gamma$. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, $\sup S$ is then the defined set symbol with argument $S$ given by the predicative $\sigma$, and it is used properly where $S\subseteq p$ has a supremum, since there exactly one set satisfies $\sigma(S,z)$.

Clause maps. Suppose first that $t(u)$ is a subset of $p$ that has a supremum for every $u\in a$. By the clause bound-symbol, $\sup S$ is a defined set symbol with argument $S$ given by the predicative $\sigma$, used properly where $S\subseteq p$ has a supremum; so in the expression $\sup t(u)$ every defined set symbol is used properly for every $u\in a$, and $\sup t(u)\in p$ by the clause supremum and the conjunct $z\in p$ of $\sigma$. Hence Maps and Relations Given by Formulas §map, applied to the sets $a$ and $p$ and the expression $\sup t(u)$, gives exactly one map $f:a\to p$ with $f(u)=\sup t(u)$ for every $u\in a$. The same argument with $\iota$ and $\inf t(u)$ gives the map for the infimum.