Proof of Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset

Preliminaries. For sets $u$ and $v$, $u\setminus v$ and $u\cap v$ are sets by Sets and Maps: Ordinary Notation (iv); by The Boolean Operations on Classes, Disjointness, and the Universal Class (i), Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i) and Subclasses and Subsets (i), $u\setminus v\subseteq u$, and $u\cap v$ is a subset of $u$ and of $v$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ix), $u\setminus v$ and $u\cap v$ are the only sets $z$ satisfying the predicative formulas $\forall w\,(w\in z\Leftrightarrow(w\in u\wedge w\notin v))$ and $\forall w\,(w\in z\Leftrightarrow(w\in u\wedge w\in v))$, respectively, $w$ and $z$ being set variables. In the expressions below, $u\setminus v$ and $u\cap v$ are the defined set symbols these formulas denote, used properly at all sets $u$ and $v$; and for a map $f$ whose domain is a set $W$, the value $f(n)$ is a defined set symbol by Functions, Values of a Function, and Functions from One Class to Another (ii), used properly at every $n\in W$. So each expression given below for the values of a map is built from defined set symbols used properly at the arguments indicated, as Maps and Relations Given by Formulas (i), Maps and Relations Given by Formulas (ii) and Maps Defined by Cases (i) require. In (i) and (iv), $A_{n}\in\mathcal{P}(X)$ for $n\in\mathbb{N}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $A_{n}\subseteq X$ by The Union Set and the Power Set of a Set (ii).

Proof of (i). For $n\in\mathbb{N}$, $X\setminus A_{n}\subseteq X$ by the preliminaries, so $X\setminus A_{n}\in\mathcal{P}(X)$ by The Union Set and the Power Set of a Set (ii). By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathcal{P}(X)$ for its $a$ and $b$ and the expression $X\setminus A_{n}$, there is exactly one map $D:\mathbb{N}\to\mathcal{P}(X)$ with $D(n)=X\setminus A_{n}$ for every $n\in\mathbb{N}$; by Sequences (i), the sequences in $\mathcal{P}(X)$ are exactly the maps $\mathbb{N}\to\mathcal{P}(X)$.

Proof of (ii). For every $S\in\mathcal{A}$, $S\cap Y\subseteq Y$ by the preliminaries, so $S\cap Y\in\mathcal{P}(Y)$ by The Union Set and the Power Set of a Set (ii). By Maps and Relations Given by Formulas (i), with $\mathcal{A}$ and $\mathcal{P}(Y)$ for its $a$ and $b$ and the expression $S\cap Y$, there is exactly one map $g:\mathcal{A}\to\mathcal{P}(Y)$ with $g(S)=S\cap Y$ for every $S\in\mathcal{A}$.

Let now $Z$ be a set and $(B_{n})$ a sequence in $Z$, a map $B:\mathbb{N}\to Z$ by Sequences (i), and let $g:Z\to\mathcal{P}(Y)$ be the map just obtained for $\mathcal{A}=Z$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), $g\circ B$ is a map $\mathbb{N}\to\mathcal{P}(Y)$, a sequence in $\mathcal{P}(Y)$, with $(g\circ B)(n)=g(B_{n})=B_{n}\cap Y$ for every $n\in\mathbb{N}$, as $B_{n}\in Z$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). If $(F_{n})$ is a sequence in $\mathcal{P}(Y)$ with $F_{n}=B_{n}\cap Y$ for every $n\in\mathbb{N}$, then $F$ and $g\circ B$ both have domain $\mathbb{N}$ by Functions, Values of a Function, and Functions from One Class to Another (iii) and the same values, so $F=g\circ B$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i).

Proof of (iii). By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii) and Arithmetic and Order of the Natural Numbers (xiv), $1\in\mathbb{N}$, $2\in\mathbb{N}$ and $2=1+1$, and $1+1\neq1$ by Arithmetic and Order of the Natural Numbers (xi); so $2\neq1$. The empty set has no element by The Empty Set, the Unordered Pair and the Singleton (i), so $\emptyset\subseteq X$ by Subclasses and Subsets (i); hence $\emptyset$, $U$ and $V$ lie in $\mathcal{P}(X)$ by The Union Set and the Power Set of a Set (ii). Take $1$, $2$, $U$, $V$ and $\emptyset$ as parameters with these sets as values; the formulas $n=1$ and $n=2$ are atomic, hence predicative.

By Maps Defined by Cases (i), with $\mathbb{N}$ and $\mathcal{P}(X)$ for its $A$ and $B$, the property $n=2$, and the expressions $V$ and $\emptyset$, there is a map $h:\mathbb{N}\to\mathcal{P}(X)$ with $h(n)=V$ if $n=2$ and $h(n)=\emptyset$ otherwise. For every $n\in\mathbb{N}$, $h(n)$ is used properly by the preliminaries and lies in $\mathcal{P}(X)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). By Maps Defined by Cases (i) again, now taking $h$ as a further parameter, with the property $n=1$ and the expressions $U$ and $h(n)$, there is a map $E:\mathbb{N}\to\mathcal{P}(X)$, a sequence in $\mathcal{P}(X)$ by Sequences (i), with $E_{1}=U$ and $E_{n}=h(n)$ for every $n\in\mathbb{N}$ with $n\neq1$. As $2\neq1$, $E_{2}=h(2)=V$; and for $n\in\mathbb{N}$ with $n\neq1$ and $n\neq2$, $E_{n}=h(n)=\emptyset$. If $(E'_{n})$ is a sequence in $\mathcal{P}(X)$ with the same three properties, then $E'_{n}=E_{n}$ for every $n\in\mathbb{N}$, as $n=1$, or $n=2$, or neither; both have domain $\mathbb{N}$ by Functions, Values of a Function, and Functions from One Class to Another (iii), so $E'=E$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i).

Proof of (iv). Let $n\in\mathbb{N}$ and $u\in\mathcal{P}(X)$. Then $u\subseteq X$ by The Union Set and the Power Set of a Set (ii), and $u\cap(X\setminus A_{n})\subseteq u$ by the preliminaries, so $u\cap(X\setminus A_{n})\subseteq X$ by Subclasses and Subsets (i) and $u\cap(X\setminus A_{n})\in\mathcal{P}(X)$ by The Union Set and the Power Set of a Set (ii). By Maps and Relations Given by Formulas (ii), with $\mathcal{P}(X)$, $\mathbb{N}$ and $\mathcal{P}(X)$ for its $b$, $c$ and $d$ and the expression $u\cap(X\setminus A_{n})$ in $n$ and $u$, there is a map $g:\mathbb{N}\times\mathcal{P}(X)\to\mathcal{P}(X)$ with $g(n,u)=u\cap(X\setminus A_{n})$ for all $n\in\mathbb{N}$ and $u\in\mathcal{P}(X)$. As $X\subseteq X$ by Subclasses and Subsets (i), $X\in\mathcal{P}(X)$. By Recursion on the Natural Numbers Starting at One (i), with $\mathcal{P}(X)$, $X$ and $g$ for its $a$, $c$ and $g$, there is exactly one map $C:\mathbb{N}\to\mathcal{P}(X)$ with $C(1)=X$ and $C(n+1)=g(n,C(n))$ for every $n\in\mathbb{N}$. Since $C_{n}\in\mathcal{P}(X)$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), $g(n,C_{n})=C_{n}\cap(X\setminus A_{n})$, so $(C_{n})$ is a sequence in $\mathcal{P}(X)$ with the stated properties. If $(C'_{n})$ is a sequence in $\mathcal{P}(X)$ with $C'_{1}=X$ and $C'_{n+1}=C'_{n}\cap(X\setminus A_{n})$ for every $n\in\mathbb{N}$, then, as $C'_{n}\in\mathcal{P}(X)$, $C'_{n+1}=g(n,C'_{n})$ for every $n\in\mathbb{N}$, and $C'=C$ by the uniqueness in Recursion on the Natural Numbers Starting at One (i).

For $n\in\mathbb{N}$, $A_{n}\cap C_{n}\subseteq A_{n}\subseteq X$ by the preliminaries, so $A_{n}\cap C_{n}\subseteq X$ by Subclasses and Subsets (i) and $A_{n}\cap C_{n}\in\mathcal{P}(X)$ by The Union Set and the Power Set of a Set (ii). By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathcal{P}(X)$ for its $a$ and $b$ and the expression $A_{n}\cap C_{n}$, there is exactly one map $B:\mathbb{N}\to\mathcal{P}(X)$, that is, by Sequences (i), exactly one sequence $(B_{n})$ in $\mathcal{P}(X)$, with $B_{n}=A_{n}\cap C_{n}$ for every $n\in\mathbb{N}$.

Proof of (v). $\mathcal{G}$ is a set, being a subset, by Subclasses and Subsets (i). By Sequences (i), $h$ is a map $h:\mathbb{N}\to\mathcal{P}(X)$, so by Functions, Values of a Function, and Functions from One Class to Another (iii) it is a function with $\operatorname{dom}h=\mathbb{N}$. Let $v\in\operatorname{ran}h$. By Relations, Domain, Range, Inverse and Composition (iii) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), there is a set $n$ with $(n,v)\in h$; then $n\in\operatorname{dom}h=\mathbb{N}$ by Relations, Domain, Range, Inverse and Composition (ii) and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), and $v=h_{n}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), so $v\in\mathcal{G}$ by hypothesis. Hence $\operatorname{ran}h\subseteq\mathcal{G}$ by Subclasses and Subsets (i), so $h:\mathbb{N}\to\mathcal{G}$ by Functions, Values of a Function, and Functions from One Class to Another (iii); that is, by Sequences (i), $(h_{n})$ is a sequence in $\mathcal{G}$.