Proof of Toolkit for AL2

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). By Negatives, Differences, Reciprocals and Quotients (i), $-x$ is the element $w\in r$ with $x+w=0$. Hence $x+(-x)=0$.

Proof of (ii). Let $s\in X^{n}$. By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $s:[n]\to X$ is a map, so its range lies in $X\subseteq Y$ and $s:[n]\to Y$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)). So $s\in Y^{n}$ by Tuples in a Set: the Set of n-Tuples and Their Components (ii). Hence $X^{n}\subseteq Y^{n}$ (Subclasses and Subsets (i)).

Proof of (iii). Every element of $b\times b$ is a pair $(u,v)$ with $u,v\in b\subseteq a$ (The Cartesian Product of Two Classes (i)), so $b\times b\subseteq a\times a$. Since $\ast:a\times a\to a$ is a map, Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vi) shows that $\ast|_{b\times b}:b\times b\to a$ is a map with

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

which is the asserted equation. Every element of the range of $\ast|_{b\times b}$ is one of these values (Relations, Domain, Range, Inverse and Composition (iii), Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii)), and they lie in $b$ by hypothesis. So the range is contained in $b$, and $\ast|_{b\times b}:b\times b\to b$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)).

Proof of (iv). As $C\subseteq B$, every element $(a,c)$ of $A\times C$ lies in $A\times B$ (The Cartesian Product of Two Classes (i)), so $A\times C\subseteq A\times B$, and by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vi) $F|_{A\times C}:A\times C\to B$ is a map with $(F|_{A\times C})((a,c))=F((a,c))$ for $a\in A$ and $c\in C$. These values lie in $C$ by hypothesis, and they make up the range (Relations, Domain, Range, Inverse and Composition (iii), Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii)); so $F|_{A\times C}:A\times C\to C$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)).

Proof of (v). Let $\iota=\mathrm{id}_{Y}$ be the identity on $Y$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii) it is a map $Y\to Y$ with $\iota(y)=y$ for $y\in Y$; its range lies in $Y\subseteq X$, so $\iota:Y\to X$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)). It satisfies $\iota(e)=e$ and, for $x,y\in Y$, $\iota(x\diamond y)=x\diamond y=x\ast y=\iota(x)\ast\iota(y)$, since $x\diamond y\in Y$. So Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vi), applied to the operation $\diamond$ on $Y$ with neutral element $e$, the operation $\ast$ on $X$ with neutral element $e$, the map $\iota:Y\to X$ and $f:A\to Y$, gives

$$\iota\Bigl(\mathop{\diamond}\limits_{x\in A}f(x)\Bigr)=\mathop{\ast}\limits_{x\in A}\iota(f(x)).$$

The element $\mathop{\diamond}\limits_{x\in A}f(x)$ is an iterated operation of $\diamond$ on $Y$, so it lies in $Y$ (Sums and Products over a Finite Set and over an Interval (i), Sums and Products over a Finite Set and over an Interval (ii)) and is fixed by $\iota$. On the right, $\iota\circ f=f$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iv), $f$ being a map $A\to Y$; and $f:A\to X$ is a map, as $Y\subseteq X$. This is the asserted equation.

Proof of (vi). By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $x:[m]\to Y$ is a map, and so is $x:[m]\to X$, as $Y\subseteq X$. If $m=0$, the interval $\{1,\dots,0\}=[0]$ is empty (Intervals of Natural Numbers (ii), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)), so by Sums and Products over a Finite Set and over an Interval (iv) and Sums and Products over a Finite Set and over an Interval (ii) both sides equal the neutral element $e$. If $m\neq0$, then $m\in\mathbb{N}$ (The Set of Natural Numbers and the Number One (i)), and Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (iv), applied to $\diamond$ on $Y$ and to $\ast$ on $X$, gives

$$\mathop{\diamond}\limits_{k=1}^{m}x_{k}=\mathop{\diamond}\limits_{k\in[m]}x_{k},\qquad\mathop{\ast}\limits_{k=1}^{m}x_{k}=\mathop{\ast}\limits_{k\in[m]}x_{k}.$$

As $[m]$ is finite (Order and Arithmetic of ℕ₀ in Flat Form (vii)), the right-hand sides agree by (v) with $A=[m]$ and $f=x$.

Proof of (vii). By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $\lambda:[n]\to K$ and $v:[n]\to V'$ are maps; and $v\in V^{n}$ by (ii), so $v:[n]\to V$ is a map as well. By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), applied with $S=[n]$, the maps $\lambda$ and $v$ and the scalar multiplication of $V'$, respectively of $V$, there is exactly one map $t':[n]\to V'$ with $t'(k)=\lambda_{k}v_{k}$, the scalar multiple taken in $V'$, and exactly one map $t:[n]\to V$ with $t(k)=\lambda_{k}v_{k}$, taken in $V$; these are the tuples of terms formed in $V'$ and in $V$. Since $V'\subseteq V$, also $t':[n]\to V$ is a map (Functions, Values of a Function, and Functions from One Class to Another (iii)), and for $k\in[n]$ we have $\lambda_{k}\in K$ and $v_{k}\in V'$, so $t'(k)=t(k)$ by hypothesis. Hence $t'=t$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii).

Operations on linear maps. In the next three proofs, a map $F$ whose values are fixed at the elements of a product is obtained from Maps from Functional Predicative Relations, and Families of Sections (ii); the formulas used there quantify over set variables only, and their atoms, of the forms $x=(S,T)$, $(v,a)\in S$ and $((a,b),y)\in P$, are 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 (ii), 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); so these formulas are predicative. For a map $S:V\to W$, $v\in V$ and a set $a$, $(v,a)\in S$ holds exactly when $a=S(v)$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii)); for a map $P$ on a product and a pair $(a,b)$ in its domain, $((a,b),y)\in P$ holds exactly when $y=P((a,b))$ (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x)); and ordered pairs of sets are equal only if their components are (The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i)).

Proof of (viii). Write $L=\mathcal{L}(V,W)$, a set by Operations on Linear Maps (i). For $S,T\in L$, the sum $S+T$ is a map $V\to W$ with $(S+T)(v)=Sv+Tv$ (Operations on Linear Maps (ii)), and it is linear: for $u,v\in V$ and $\lambda\in K$, by the linearity of $S$ and $T$ (Linear Maps, Linear Operators and Isomorphisms of Vector Spaces (i)) and Vector Space over a Field (i), Vector Space over a Field (ii) and Vector Space over a Field (vii) in $W$,

$$(S+T)(u+v)=(Su+Sv)+(Tu+Tv)=(Su+Tu)+(Sv+Tv)=(S+T)(u)+(S+T)(v),$$ $$(S+T)(\lambda v)=\lambda Sv+\lambda Tv=\lambda(Sv+Tv)=\lambda\,(S+T)(v).$$

So $S+T\in L$. Let $\psi(x,F)$ be the formula

$$\exists S\,\exists T\,\Bigl(x=(S,T)\wedge\forall v\,\bigl(v\in V\Rightarrow\exists a\,\exists b\,\exists y\,((v,a)\in S\wedge(v,b)\in T\wedge((a,b),y)\in{+_{W}}\wedge(v,y)\in F)\bigr)\Bigr),$$

with parameters $V$ and the addition $+_{W}$ of $W$; it is predicative. Let $S,T\in L$ and $F\in L$. By the facts recalled above, $\psi((S,T),F)$ holds if and only if $F(v)=Sv+Tv$ for every $v\in V$, that is, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii), if and only if $F=S+T$. So every element of $L\times L$ has exactly one $F\in L$ with $\psi$, and Maps from Functional Predicative Relations, and Families of Sections (ii), applied to the classes $L\times L$ and $L$, gives a map $A:L\times L\to L$ with $\psi(x,A(x))$ for every $x\in L\times L$. Thus $A((S,T))=S+T$ for all $S,T\in L$, and $A$ is a binary operation on the set $L$ (Binary Operations on a Set (i)).

Proof of (ix). Again $L=\mathcal{L}(V,W)$. For $\lambda\in K$ and $T\in L$, $\lambda T$ is a map $V\to W$ with $(\lambda T)(v)=\lambda\,Tv$ (Operations on Linear Maps (iii)), and it is linear: for $u,v\in V$ and $\mu\in K$, by the linearity of $T$, Vector Space over a Field (vii), Vector Space over a Field (v) and the commutativity of the multiplication of the field $K$ (Fields (i)),

$$(\lambda T)(u+v)=\lambda(Tu+Tv)=\lambda Tu+\lambda Tv,\qquad(\lambda T)(\mu v)=\lambda(\mu Tv)=(\lambda\mu)Tv=(\mu\lambda)Tv=\mu(\lambda Tv).$$

So $\lambda T\in L$. Let $\sigma_{W}:K\times W\to W$ be the scalar multiplication of $W$, and let $\psi(x,F)$ be the predicative formula

$$\exists\lambda\,\exists T\,\Bigl(x=(\lambda,T)\wedge\forall v\,\bigl(v\in V\Rightarrow\exists b\,\exists y\,((v,b)\in T\wedge((\lambda,b),y)\in\sigma_{W}\wedge(v,y)\in F)\bigr)\Bigr),$$

with parameters $V$ and $\sigma_{W}$. For $\lambda\in K$, $T\in L$ and $F\in L$, $\psi((\lambda,T),F)$ holds if and only if $F(v)=\lambda\,Tv$ for every $v\in V$, that is, if and only if $F=\lambda T$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). So every element of $K\times L$ has exactly one $F\in L$ with $\psi$, namely $\lambda T$, and Maps from Functional Predicative Relations, and Families of Sections (ii) gives a map $M:K\times L\to L$ with $M((\lambda,T))=\lambda T$.

Proof of (x). Write $L=\mathcal{L}(V)$. For $S,T\in L$, $ST:V\to V$ is a map with $(ST)(v)=S(Tv)$ (Operations on Linear Maps (iv)), and it is linear: for $u,v\in V$ and $\lambda\in K$, by the linearity of $T$ and then of $S$ (Linear Maps, Linear Operators and Isomorphisms of Vector Spaces (i)),

$$(ST)(u+v)=S(Tu+Tv)=S(Tu)+S(Tv),\qquad(ST)(\lambda v)=S(\lambda Tv)=\lambda S(Tv).$$

So $ST\in L$. Let $\psi(x,F)$ be the predicative formula

$$\exists S\,\exists T\,\Bigl(x=(S,T)\wedge\forall v\,\bigl(v\in V\Rightarrow\exists b\,\exists y\,((v,b)\in T\wedge(b,y)\in S\wedge(v,y)\in F)\bigr)\Bigr),$$

with parameter $V$. For $S,T,F\in L$, $\psi((S,T),F)$ holds if and only if $F(v)=S(Tv)$ for every $v\in V$, that is, if and only if $F=ST$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). So Maps from Functional Predicative Relations, and Families of Sections (ii) gives a map $C:L\times L\to L$ with $C((S,T))=ST$, a binary operation on the set $L$ (Operations on Linear Maps (i), Binary Operations on a Set (i)).

Proof of (xi). By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (vi), $F^{-1}:B\to A$ is a (bijective) map with $F\circ F^{-1}=\mathrm{id}_{B}$ and $F^{-1}\circ F=\mathrm{id}_{A}$. For $w\in B$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii) and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii),

$$F(F^{-1}(w))=(F\circ F^{-1})(w)=\mathrm{id}_{B}(w)=w,$$

and likewise $F^{-1}(F(v))=(F^{-1}\circ F)(v)=\mathrm{id}_{A}(v)=v$ for $v\in A$.

Proof of (xii). By Subclasses and Subsets (i), every set $z$ with $z\in X$ satisfies $z\in Y$, and conversely. So $z\in X$ holds if and only if $z\in Y$ holds, for every set $z$, and $X=Y$ by Axiom of Extensionality for Classes.

Proof of (xiii). A bijection $G:A\to B$ is a map (Injective, Surjective and Bijective Functions between Classes (iii)), so $G(u)\in B$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (i).

Proof of (xiv). On either side of the equivalence, $i$ is an element of a class, hence a set (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)); it therefore suffices to consider a set $i$. By The Boolean Operations on Classes, Disjointness, and the Universal Class (i), $A\setminus\{j\}$ is the class of the sets $u$ with $u\in A$ and $u\notin\{j\}$, so $i\in A\setminus\{j\}$ if and only if $i\in A$ and $i\notin\{j\}$ (Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i)). The only element of $\{j\}$ is $j$ (The Empty Set, the Unordered Pair and the Singleton (iii)), so $i\notin\{j\}$ if and only if $i\neq j$.

Proof of (xv). By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $f,g:[n]\to X$ are maps, and $[n]$ is a set (Tuples in a Set: the Set of n-Tuples and Their Components (i)). By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), applied with $S=[n]$, $Y=Z=W=X$ and the map $\ast:X\times X\to X$ (Binary Operations on a Set (i)), there is a map $s:[n]\to X$ with $s(k)=\ast((f(k),g(k)))=f_{k}\ast g_{k}$ for every $k\in[n]$. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and Tuples in a Set: the Set of n-Tuples and Their Components (i), $s\in X^{n}$.

Proof of (xvi). By Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i), applied with $S=[n]$ and $Y=X$, there is a map $s:[n]\to X$ with $s(k)=c$ for every $k\in[n]$; and $s\in X^{n}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and Tuples in a Set: the Set of n-Tuples and Their Components (i).

Proof of (xvii). Let $\psi(k,y)$ be the formula $(k=j\wedge y=a)\vee(\neg\,k=j\wedge y=b)$, with parameters $j$, $a$ and $b$. It is built from equations between set variables by connectives only, so it is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). For $k\in[n]$, the sets $y\in X$ with $\psi(k,y)$ are exactly $y=a$ if $k=j$ and $y=b$ if $k\neq j$, and $a,b\in X$; so there is exactly one. By Maps from Functional Predicative Relations, and Families of Sections (ii), applied to the classes $[n]$ and $X$, there is a map $s:[n]\to X$ with $\psi(k,s(k))$ for every $k\in[n]$. As $j\in[n]$, this gives $s_{j}=a$, and $s_{k}=b$ for $k\in[n]$ with $k\neq j$. Finally $s\in X^{n}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i) and Tuples in a Set: the Set of n-Tuples and Their Components (i).

Proof of (xviii). By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $s,t:[n]\to X$ are maps, and their values agree at every $k\in[n]$; so $s=t$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii).

Proof of (xix). Since $[0]=\emptyset$ (Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)) and $j\in[n]$, we have $n\neq0$, so $n\in\mathbb{N}$ (The Set of Natural Numbers and the Number One (i)). By Order and Arithmetic of ℕ₀ in Flat Form (vi), $n=m+1$ for some $m\in\mathbb{N}_{0}$.

A formula for linear independence. Let $K$ be a field and $V$ a vector space over $K$, with addition $+_{V}$, scalar multiplication $\mu:K\times V\to V$ and zero vector $0_{V}$. For set variables $q$ and $c$ let $\Lambda(q,c)$ be the formula

$$\forall\lambda\,\forall s\,\forall t\,\forall z\,\Bigl(\bigl(\lambda\in K^{q}\wedge s=[q]\wedge t:s\to V\wedge\forall i\,\bigl(i\in s\Rightarrow\exists a\,\exists b\,\exists y\,((i,a)\in\lambda\wedge(i,b)\in c\wedge((a,b),y)\in\mu\wedge(i,y)\in t)\bigr)\wedge\Sigma(z,s,t)\wedge z=0_{V}\bigr)\Rightarrow\forall i\,\bigl(i\in s\Rightarrow(i,0)\in\lambda\bigr)\Bigr),$$

where $\Sigma(z,s,t)$ says that $s$ is finite, $t:s\to V$ is a map and $z$ is the iterated operation of $+_{V}$ over $s$ of $t$, and $0$ is the zero of $K$. Its parameters are $K$, $0$, $V$, $\mu$, $+_{V}$ and $0_{V}$. It quantifies over set variables only, and its parts are predicative: $\lambda\in K^{q}$, written $\exists r\,(r=K^{q}\wedge\lambda\in r)$, by Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (iii); $s=[q]$ by Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (ii); $t:s\to V$ 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); $\Sigma$ by Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (vii), which applies because $+_{V}$ is associative and commutative with neutral element $0_{V}$ (Vector Space over a Field (i), Vector Space over a Field (ii), The Zero Vector, Negatives and Differences in a Vector Space (i)); and the memberships of pairs 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). So $\Lambda$ is predicative.

Let $q\in\mathbb{N}_{0}$ and $c\in V^{q}$; then $\Lambda(q,c)$ holds if and only if $c$ is linearly independent. Indeed, let $\lambda\in K^{q}$. In the antecedent $s$ must be $[q]$, a finite set (Order and Arithmetic of ℕ₀ in Flat Form (vii)); by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii) and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x) the conditions on $t$ say that $t:[q]\to V$ is a map with $t(i)=\lambda_{i}c_{i}$ for every $i\in[q]$, and exactly one such map exists (Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii), with the maps $\lambda$, $c$ and $\mu$); and $z$ must then be $\sum_{i\in[q]}t(i)$, which is $\sum_{i=1}^{q}\lambda_{i}c_{i}$ by Span of a Finite Family; Spanning Families (i) and Sums and Products over a Finite Set and over an Interval (iv), as $\{1,\dots,q\}=[q]$ (Intervals of Natural Numbers (ii)). Finally, $(i,0)\in\lambda$ says $\lambda_{i}=0$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii)). So $\Lambda(q,c)$ says that, for every $\lambda\in K^{q}$, $\sum_{i=1}^{q}\lambda_{i}c_{i}=0_{V}$ implies $\lambda_{i}=0$ for every $i\in[q]$, which is Linearly Independent and Linearly Dependent Finite Families (i).

Proof of (xx). Let $\varphi(p)$ be the condition of the statement with "$c$ linearly independent" written as $\Lambda(m+p,c)$, which is equivalent to it by the previous paragraph, since $c\in V^{m+p}$:

$$p\in\mathbb{N}_{0}\wedge\exists w\,\exists c\,\Bigl(w\in V^{p}\wedge c\in V^{m+p}\wedge\forall i\,\bigl(i\in[m]\Rightarrow c_{i}=u_{i}\bigr)\wedge\forall j\,\bigl(j\in[p]\Rightarrow c_{m+j}=w_{j}\bigr)\wedge\Lambda(m+p,c)\Bigr).$$

In this expression the components $c_{i}$, $u_{i}$, $c_{m+j}$ and $w_{j}$ (Tuples in a Set: the Set of n-Tuples and Their Components (iii)) and the sums $m+p$ and $m+j$ (Addition on Omega (i)) are defined set symbols, each used where the conjuncts and guards before it make it defined, since $m\in\mathbb{N}_{0}$ and $u\in V^{m}$; the conditions $i\in[m]$, $j\in[p]$, $w\in V^{p}$ and $c\in V^{m+p}$ are written with the predicative formulas of Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (ii) and Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (iii); and no quantifier is applied to a class variable. Its parameters are the sets $m$ and $u$, $\mathbb{N}_{0}$, the addition of $\mathbb{N}_{0}$, and those of $\Lambda$. So $\varphi$ is predicative (Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i)), and the class $A=\{p:\varphi(p)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) satisfies $p\in A$ if and only if $\varphi(p)$, for every set $p$. For a class $p$ that is not a set, both sides fail, since elements of classes are sets (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)). So $A$ is as asserted.

Proof of (xxi). Let $\varphi(q)$ be the formula

$$q\in\mathbb{N}_{0}\wedge\exists c\,\bigl(c\in W^{q}\wedge\Lambda(q,c)\bigr),$$

with parameters $\mathbb{N}_{0}$, $W$ and those of $\Lambda$, in which $c\in W^{q}$ is written $\exists r\,(r=W^{q}\wedge c\in r)$ with the predicative formula of Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (iii). It quantifies over set variables only, so it is predicative. Here $W$ is a set, being a subclass of the set $V$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)); so for $q\in\mathbb{N}_{0}$ and $c\in W^{q}$ we have $c\in V^{q}$ by (ii), so linear independence of $c$ is defined and, by the paragraph on $\Lambda$, holds exactly when $\Lambda(q,c)$ does. Hence $\varphi(q)$ holds exactly when $q\in\mathbb{N}_{0}$ and some $c\in W^{q}$ is linearly independent. The class $A=\{q:\varphi(q)\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) satisfies $q\in A$ if and only if $\varphi(q)$ for every set $q$, and both sides fail for a class $q$ that is not a set, since elements of classes are sets (Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i)).

Proof of (xxii). Let $l$ be a set variable other than $x_{0}$ and $x_{1}$, and let $\psi$ be the formula

$$\exists l\,\bigl(l\in A\wedge(l,x_{0})\in F\wedge(l,x_{1})\in G\bigr).$$

Its atom $l\in A$ is a formula, and $(l,x_{0})\in F$ and $(l,x_{1})\in G$ are predicative and hold exactly when the ordered pairs of the values are elements of $F$ and of $G$ (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)). Conjunction and a quantifier over the set variable $l$ preserve predicativity (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)), so $\psi$ is predicative; its free variables are among $x_{0}$, $x_{1}$, $A$, $F$ and $G$, and under every assignment of sets to $x_{0}$ and $x_{1}$ it reads "there is a set $l\in A$ with $(l,x_{0})\in F$ and $(l,x_{1})\in G$" (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (iv)). So $\psi$ expresses the condition (Conditions Expressed by a Predicative Formula, and Guards (ii)).