Proof of Toolkit for AL1

Routine facts about maps, arithmetic and order in $\mathbb{N}_{0}$, and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi)).

Proof of (i). Every element of $A$ is an element of $A$, so $A\subseteq A$ by Subclasses and Subsets (i); as $A$ is a set, it is a subset of itself.

Proof of (ii). The empty set has no element (The Empty Set, the Unordered Pair and the Singleton (i)), whereas $g\in H$. Hence $H\neq\emptyset$.

Proof of (iii). By The Boolean Operations on Classes, Disjointness, and the Universal Class (ii), $X\cap Y$ has no element, and neither has $\emptyset$ (The Empty Set, the Unordered Pair and the Singleton (i)). So, for every set $z$, $z\in X\cap Y$ holds if and only if $z\in\emptyset$ holds, both being false, and $X\cap Y=\emptyset$ by Axiom of Extensionality for Classes. (For sets $X$ and $Y$ this is part of Monotone Sequences of Sets, Unions of Traces, and Disjointness of Smaller Sets (iv).)

Proof of (iv). The class $S$ is a set, as a subclass of the set $M$. Every element of $S\times S$ is a pair $(u,v)$ with $u,v\in S\subseteq M$ (The Cartesian Product of Two Classes (i)), so $S\times S\subseteq M\times M$; since $\ast:M\times M\to M$ is a map (Binary Operations on a Set (i)), its restriction $\ast|_{S\times S}:S\times S\to M$ is a map with

$$(\ast|_{S\times S})((u,v))=u\ast v\qquad(u,v\in S).$$

Every element of its range is such a value (Relations, Domain, Range, Inverse and Composition (iii)), and these values lie in $S$ by hypothesis. So the range is contained in $S$, and $\ast|_{S\times S}:S\times S\to S$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)), that is, a binary operation on $S$.

Proof of (v). Since $u,v\in S\subseteq M$, the pair $(u,v)$ lies in $S\times S$ and in $M\times M=\operatorname{dom}\ast$. Hence $(\ast|_{S\times S})((u,v))=\ast((u,v))=u\ast v$, the restriction having the values of $\ast$ on $S\times S$.

Proof of (vi). Write $\ast_{S}=\ast|_{S\times S}$, a binary operation on $S$ by (iv). Let $u,v,w\in S$; then $u\ast v\in S$ and $v\ast w\in S$, and all of $u,v,w$ lie in $M$. Using (v) twice on each side and the associativity of $\ast$ on $M$ (Associative and Commutative Binary Operations, and Neutral Elements (i)),

$$(u\ast_{S}v)\ast_{S}w=(u\ast v)\ast w=u\ast(v\ast w)=u\ast_{S}(v\ast_{S}w).$$

So $\ast_{S}$ is associative.

Proof of (vii). Again $\ast_{S}=\ast|_{S\times S}$ is a binary operation on $S$ by (iv), and $e\in S$. For $x\in S$ we have $x\in M$, so by (v) and Associative and Commutative Binary Operations, and Neutral Elements (iii),

$$e\ast_{S}x=e\ast x=x,\qquad x\ast_{S}e=x\ast e=x .$$

Hence $e$ is a neutral element of $\ast_{S}$.

Proof of (viii). As $n\in\mathbb{N}$, this is Powers with Exponents in the Natural Numbers with Zero (i).

Proof of (ix). By (viii) and Iterated Operations: Finite Sums and Finite Products (i), $x^{n}$ is the iterated operation of the map $[n]\to X$, $k\mapsto x$. The map $[n]\times\{x\}:[n]\to X$ has value $x$ at every $k\in[n]$, so it is this map, and the equation follows.

Proof of (x). By Powers with Exponents in the Natural Numbers with Zero (ii), $x^{0}$ is the neutral element of $\cdot$, which is unique by A Binary Operation Has at Most One Neutral Element (i). As $e$ is a neutral element, $x^{0}=e$.

Proof of (xii). Let $j\in[m]$. Then $n+j\in[n+m]$ by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] (ii) (with $n$ and $m$ interchanged), and both $([m]\times\{x\})(j)$ and $([n+m]\times\{x\})(n+j)$ equal $x$, which proves the first assertion. For the second, $[n]\subseteq[n+m]$ by Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] (i) (with $n$ and $m$ interchanged). Let $c=[n+m]\times\{x\}$. Its restriction $c|_{[n]}$ and $[n]\times\{x\}$ are maps $[n]\to X$ with value $x$ at every $k\in[n]$, so $c|_{[n]}=[n]\times\{x\}$. By Iterated Operations: Finite Sums and Finite Products (ii), the left side of the equation is the iterated operation of $c|_{[n]}=[n]\times\{x\}$, which is the right side.

Proof of (xi). This is the second assertion of (xii) with $m=1\in\mathbb{N}$.

Proof of (xiii). By Monoids (i), $\cdot$ is a binary operation on $M$ with a neutral element, so by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iii) there is a map $q:\mathbb{N}_{0}\to M$ with $q(m)=x^{m}$ for every $m\in\mathbb{N}_{0}$. Hence $x^{n}=q(n)\in M$.

Typed terms for the four predicative clauses. Let $(M,\cdot)$ be a monoid. Its operation has a neutral element (Monoids (i)), so the map $p:M\times\mathbb{N}_{0}\to M$, $p((y,m))=y^{m}$, exists by Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ x^m (ii). Let $\gamma$ be the guard $x_{0}\in\mathbb{N}_{0}$. Under $\gamma$, $x_{0}$ and the named elements of $\mathbb{N}_{0}$ are terms of type $\mathbb{N}_{0}$, the named elements of $M$ are terms of type $M$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (ii)), and, forming pairs and values of $p$, of the multiplication of $\mathbb{N}_{0}$ and of the operation $\cdot:M\times M\to M$ (Binary Operations on a Set (i), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iv), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii)), so are $y^{x_{0}}=p((y,x_{0}))$, $y^{a x_{0}}=p((y,a\cdot x_{0}))$ and $st$, for named $y\in M$ and $a\in\mathbb{N}_{0}$ and terms $s,t$ of type $M$.

Now let $s$ and $t$ be terms of type $M$ under $\gamma$. The condition "$\gamma$ and $s=t$" is expressed by a predicative formula $\psi$ (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v)). The formula $\neg(x_{0}\in\mathbb{N}_{0})\vee\psi$ is predicative, its free variables are $x_{0}$ and the parameters listed in the statement, and under every assignment of a set to $x_{0}$

$$\neg(x_{0}\in\mathbb{N}_{0})\vee\psi\iff\bigl(x_{0}\in\mathbb{N}_{0}\Rightarrow s=t\bigr),$$

since if $x_{0}\notin\mathbb{N}_{0}$ both sides hold, and if $x_{0}\in\mathbb{N}_{0}$ both say $s=t$. So it expresses the condition "if $x_{0}\in\mathbb{N}_{0}$, then $s=t$".

Proof of (xiv). Apply the paragraph above with $s=w^{x_{0}}$ and $t=u^{a x_{0}}$.

Proof of (xv). Apply it with $s=u^{x_{0}}$ and $t=c$, a term of type $M$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (ii).

Proof of (xvi). Apply it with $s=u^{x_{0}}v$ and $t=vu^{x_{0}}$.

Proof of (xvii). Apply it with $s=w^{x_{0}}$ and $t=u^{x_{0}}v^{x_{0}}$.

Proof of (xviii). Let $\varphi(r)$ be the formula

$$r\in\mathbb{N}_{0}\wedge\exists q\,\exists s\,\exists t\,\exists z\,\bigl(q\in\mathbb{Z}\wedge((q,c),s)\in{\cdot}\wedge(r,t)\in f\wedge((s,t),z)\in{+}\wedge\forall w\,(w\in z\Leftrightarrow w\in m)\bigr),$$

with the parameters $\mathbb{N}_{0}$, $\mathbb{Z}$, its product $\cdot$ and sum $+$, $c$, $f$ and $m$. It quantifies over set variables only, the ordered pairs being defined set symbols, so it is predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)). Let $r$ be a set with $r\in\mathbb{N}_{0}$. For $q\in\mathbb{Z}$: $((q,c),s)\in{\cdot}$ holds exactly for $s=q\cdot c$, as $c\in\mathbb{Z}$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi)); $(r,t)\in f$ holds exactly for $t=f(r)$, which lies in $\mathbb{Z}$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)); then $((s,t),z)\in{+}$ holds exactly for $z=q\cdot c+f(r)$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi)); and the last conjunct says $z=m$ (Axiom of Extensionality for Classes). So $\varphi(r)$ holds if and only if $r\in\mathbb{N}_{0}$ and $m=q\cdot c+f(r)$ for some $q\in\mathbb{Z}$. The class $S=\{r:\varphi(r)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) therefore has the stated elements.

Proof of (xix). Let $e$ be the identity of $G$ and let $\varphi(p)$ be the formula

$$\exists g\,\exists k\,\exists y\,\exists z\,\bigl(g\in G\wedge k\in G\wedge p=(g,k)\wedge y\in G\wedge((g,y),e)\in{\cdot}\wedge((y,g),e)\in{\cdot}\wedge((y,k),z)\in{\cdot}\wedge z\in H\bigr),$$

with the parameters $G$, its operation $\cdot$, $e$ and $H$. It quantifies over set variables only, the ordered pairs being defined set symbols, so it is predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)). For $g,k,y\in G$: $((g,y),e)\in{\cdot}$ and $((y,g),e)\in{\cdot}$ say $gy=e$ and $yg=e$, and $((y,k),z)\in{\cdot}$ says $z=yk$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi)). By Uniqueness of the Identity Element and of Inverses in a Group (ii), the only $y\in G$ with $gy=yg=e$ is $g^{-1}$. So, for every set $p$, $\varphi(p)$ holds if and only if $p=(g,k)$ for some $g,k\in G$ with $g^{-1}k\in H$, and the class $R=\{p:\varphi(p)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) has the stated elements.