Proof of The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻

Proof of (i). Let $a,z\in\mathbb{R}$. As $\le$ is total, $a\le0$ or $0\le a$. Suppose $z=\max\{a,0\}$. By The Maximum and Minimum of Two Elements of a Total Order (ii), $z=0$ if $a\le0$ and $z=a$ if $0\le a$; and $a\le z$ and $0\le z$ by The Maximum and Minimum of Two Elements of a Total Order (iii). Conversely, suppose ($z=a$ or $z=0$), $a\le z$ and $0\le z$. If $z=a$, then $0\le a$, so $\max\{a,0\}=a=z$ by The Maximum and Minimum of Two Elements of a Total Order (ii); if $z=0$, then $a\le0$, so $\max\{a,0\}=0=z$ by The Maximum and Minimum of Two Elements of a Total Order (ii).

Proof of (ii). Let $f\in\mathbb{R}^{X}$. By Positive Part, Negative Part and Absolute Value of a Real-Valued Function (i), $f^{+}$ is a function $X\to\mathbb{R}$ with $f^{+}(x)=\max\{f(x),0\}$ for every $x\in X$, and every function $g:X\to\mathbb{R}$ with these values equals $f^{+}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv). So, for every set $g$, $g=f^{+}$ if and only if $g$ is a function $X\to\mathbb{R}$ and $g(x)=\max\{f(x),0\}$ for every $x\in X$; by (i), applied to $a=f(x)$ and $z=g(x)$, the latter holds if and only if, for every $x\in X$, ($g(x)=f(x)$ or $g(x)=0$), $f(x)\le g(x)$ and $0\le g(x)$. Likewise, by Positive Part, Negative Part and Absolute Value of a Real-Valued Function (ii), $g=f^{-}$ if and only if $g$ is a function $X\to\mathbb{R}$ and, for every $x\in X$, with $w=-f(x)$, ($g(x)=w$ or $g(x)=0$), $w\le g(x)$ and $0\le g(x)$; here, for $y\in\mathbb{R}$, $w=-y$ if and only if $w\in\mathbb{R}$ and $y+w=0$, by Negatives, Differences, Reciprocals and Quotients (i).

Let $\mu$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii); by it and The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $f\in\mathbb{R}^{X}$ if and only if $\mu(f,X,\mathbb{R})$, and $g$ is a function $X\to\mathbb{R}$ if and only if $\mu(g,X,\mathbb{R})$. For a function $h$ with domain $X$, $x\in X$ and a set $y$, $h(x)=y$ if and only if $(x,y)\in h$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)). Hence the condition "$f\in\mathbb{R}^{X}$ and $g=f^{+}$" is expressed by

$$\mu(f,X,\mathbb{R})\wedge\mu(g,X,\mathbb{R})\wedge\forall x\,\bigl(x\in X\Rightarrow\exists y\,\exists z\,((x,y)\in f\wedge(x,z)\in g\wedge(z=y\vee z=0)\wedge(y,z)\in{\le}\wedge(0,z)\in{\le})\bigr),$$

and the condition "$f\in\mathbb{R}^{X}$ and $g=f^{-}$" by the same formula with the part after $\exists y\,\exists z$ replaced by

$$\exists w\,\bigl((x,y)\in f\wedge w\in\mathbb{R}\wedge((y,w),0)\in{+}\wedge(x,z)\in g\wedge(z=w\vee z=0)\wedge(w,z)\in{\le}\wedge(0,z)\in{\le}\bigr),$$

where $((y,w),0)\in{+}$ says $y+w=0$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi)). Both formulas are predicative: $\mu$ is by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), the memberships of ordered pairs are by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), and all other quantifiers are over set variables.

Proof of (iii). For every $f\in\mathbb{R}^{X}$, $f^{+}\in\mathbb{R}^{X}$, and by (ii), under the predicative condition $\mu(f,X,\mathbb{R})$, $f^{+}$ is the only set $g$ satisfying a predicative formula; so $f^{+}$ may be eliminated through that formula (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii)) and $f\mapsto f^{+}$ is given by an expression in $f$. By Maps and Relations Given by Formulas (i), with $a=b=\mathbb{R}^{X}$ and $t(f)=f^{+}$, there is exactly one function $P:\mathbb{R}^{X}\to\mathbb{R}^{X}$ with $P(f)=f^{+}$ for every $f\in\mathbb{R}^{X}$; in the same way, with $t(f)=f^{-}$, there is exactly one such $N$. For $f\in\mathbb{R}^{X}$ and a set $g$, $(f,g)\in P$ if and only if $P(f)=g$, that is, $g=f^{+}$, and $(f,g)\in N$ if and only if $g=f^{-}$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i).