Proof of The Reciprocal and the Quotient of Real-Valued Maps with a Nonvanishing Denominator Are Maps

Proof of (ii). Let $t\in E$. Then $f(t)\in\mathbb{R}$ and $\chi(t)\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), and $\chi(t)\neq0$. The set $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), so the quotient $f(t)/\chi(t)=f(t)\cdot\chi(t)^{-1}$ is defined by Negatives, Differences, Reciprocals and Quotients (ii) and lies in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (ii). For the same reason, Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (viii) gives a predicative formula $\psi$, with $\mathbb{R}$ and its operations, $0$, $1$ and order as the values of its parameters, that holds if and only if $x\in\mathbb{R}\wedge y\in\mathbb{R}\wedge y\neq0\wedge z=x/y$. Let $\psi'$ be $\psi$ with the set variables $x$ and $y$ replaced by set variables $x'$ and $y'$ occurring neither in $\psi$ nor among $t$, $f$ and $\chi$, as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i); it is predicative, and it holds if and only if $x'\in\mathbb{R}\wedge y'\in\mathbb{R}\wedge y'\neq0\wedge z=x'/y'$. Let $\theta(z,t)$ be the formula $\exists x'\,\exists y'\,((t,x')\in f\wedge(t,y')\in\chi\wedge\psi')$, predicative 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 of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), no quantifier being applied to a class variable. For $t\in E$, $(t,x')\in f$ if and only if $x'=f(t)$, and $(t,y')\in\chi$ if and only if $y'=\chi(t)$, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i); so $f(t)/\chi(t)$ is the only set $z$ with $\theta(z,t)$. Thus $f(t)/\chi(t)$ is a defined set symbol with argument $t$, introduced by $\theta$ and used properly where $t\in E$. By Maps and Relations Given by Formulas (i), with $E$ and $\mathbb{R}$ for its $a$ and $b$, there is exactly one map $f/\chi:E\to\mathbb{R}$ with $(f/\chi)(t)=f(t)/\chi(t)$ for every $t\in E$; it is the map $t\mapsto f(t)/\chi(t)$ of Sets and Maps: Ordinary Notation (v), given by the predicative formula of Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v).

Proof of (i). The same argument, with the parameter $1\in\mathbb{R}$ in place of $f(t)$, shows that $1/\chi(t)=1\cdot\chi(t)^{-1}$ lies in $\mathbb{R}$ for every $t\in E$ and is a defined set symbol with argument $t$, used properly where $t\in E$; Maps and Relations Given by Formulas (i) gives exactly one map $1/\chi:E\to\mathbb{R}$ with $(1/\chi)(t)=1/\chi(t)$ for every $t\in E$.