Proof of Monotone Sequences of Sets, Unions of Traces, and Disjointness of Smaller Sets

Proof of (i). Let $(A_{m})$ be as there and fix $k\in\mathbb{N}$. Let $\varphi$ be the condition on the set variable $n$, with the parameters $\mathbb{N}$, $k$, the order $\le$ of $\mathbb{N}_{0}$ and the map $A$, given by

$$n\in\mathbb{N}\wedge(k\le n\Rightarrow A_{k}\subseteq A_{n}).$$

This expression quantifies over no class variable, so it is predicative by Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices (iv), and it expresses $\varphi$.

$\varphi(1)$ holds: $1\in\mathbb{N}$, and if $k\le1$, then, as $k<1$ fails by Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (ii), $k=1$ by Arithmetic and Order of the Natural Numbers (vi), so $A_{k}=A_{1}\subseteq A_{1}$. Let $n\in\mathbb{N}$ with $\varphi(n)$; then $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi). Let $k\le n+1$. By Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (iii), $k\le n$ or $k=n+1$. If $k\le n$, then $A_{k}\subseteq A_{n}$ by $\varphi(n)$, and $A_{n}\subseteq A_{n+1}$ by hypothesis, so every element of $A_{k}$ lies in $A_{n+1}$, that is, $A_{k}\subseteq A_{n+1}$ by Subclasses and Subsets (i). If $k=n+1$, then $A_{k}=A_{n+1}$. So $\varphi(n+1)$ holds. By Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i), $\varphi(n)$ holds for every $n\in\mathbb{N}$: $A_{k}\subseteq A_{n}$ whenever $k\le n$. As $k\in\mathbb{N}$ was arbitrary, this proves the clause.

Proof of (ii). Let $(A_{m})$ be as there and fix $k\in\mathbb{N}$. The condition $\varphi'$ on $n$ given by $n\in\mathbb{N}\wedge(k\le n\Rightarrow A_{n}\subseteq A_{k})$, with the same parameters, is expressed by this predicative expression, for the same reasons as above. $\varphi'(1)$ holds: if $k\le1$, then $k=1$ as above, and $A_{1}\subseteq A_{k}$. Let $n\in\mathbb{N}$ with $\varphi'(n)$, so $n+1\in\mathbb{N}$, and let $k\le n+1$; then $k\le n$ or $k=n+1$ by Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (iii). If $k\le n$, then $A_{n+1}\subseteq A_{n}$ by hypothesis and $A_{n}\subseteq A_{k}$ by $\varphi'(n)$, so $A_{n+1}\subseteq A_{k}$ by Subclasses and Subsets (i); if $k=n+1$, then $A_{n+1}=A_{k}$. So $\varphi'(n+1)$ holds, and by Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i), $A_{n}\subseteq A_{k}$ for all $n\in\mathbb{N}$ with $k\le n$. Finally, $1\le n$ for every $n\in\mathbb{N}$ by Arithmetic and Order of the Natural Numbers (x), so the case $k=1$ gives $A_{n}\subseteq A_{1}$.

Proof of (iii). The family $(A_{m}\cap Y)_{m\in\mathbb{N}}$ has the value $A_{m}\cap Y$ at each $m\in\mathbb{N}$. Let $x$ be a set. By Indexed Families of Sets and Their Union, Intersection and Product (ii), $x\in\bigcup_{m\in\mathbb{N}}(A_{m}\cap Y)$ if and only if there is $m\in\mathbb{N}$ with $x\in A_{m}\cap Y$, that is, by The Boolean Operations on Classes, Disjointness, and the Universal Class (i), with $x\in A_{m}$ and $x\in Y$. As the condition $x\in Y$ does not involve $m$, this holds if and only if there is $m\in\mathbb{N}$ with $x\in A_{m}$, and $x\in Y$; that is, by Indexed Families of Sets and Their Union, Intersection and Product (ii), if and only if $x\in\bigcup_{m\in\mathbb{N}}A_{m}$ and $x\in Y$, which by The Boolean Operations on Classes, Disjointness, and the Universal Class (i) means $x\in\Big(\bigcup_{m\in\mathbb{N}}A_{m}\Big)\cap Y$. The two classes have the same elements, so they are equal by Axiom of Extensionality for Classes.

Proof of (iv). Let $A$ and $B$ be sets. By The Boolean Operations on Classes, Disjointness, and the Universal Class (i), a set $x$ lies in $A\cap B$ if and only if $x\in A$ and $x\in B$, and every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (i); so $A\cap B$ has no element if and only if no set is an element of both $A$ and $B$, which by The Boolean Operations on Classes, Disjointness, and the Universal Class (ii) means that $A$ and $B$ are disjoint. If $A\cap B=\emptyset$, then $A\cap B$ has no element, since $\emptyset$ has none by The Empty Set, the Unordered Pair and the Singleton (i). Conversely, if $A\cap B$ has no element, then $A\cap B=\emptyset$ by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique (ii), every class with no element being equal to the set with no element.

Proof of (v). Let $m,k\in\mathbb{N}$ with $m\neq k$, and suppose a set $x$ lies in $C_{m}\cap C_{k}$. By The Boolean Operations on Classes, Disjointness, and the Universal Class (i), $x\in C_{m}$ and $x\in C_{k}$; as $C_{m}\subseteq A_{m}$ and $C_{k}\subseteq A_{k}$, $x\in A_{m}$ and $x\in A_{k}$ by Subclasses and Subsets (i), so $x$ is an element of both $A_{m}$ and $A_{k}$. But $A_{m}\cap A_{k}=\emptyset$, so by (iv) no set is an element of both, a contradiction. Hence no set is an element of both $C_{m}$ and $C_{k}$, and $C_{m}\cap C_{k}=\emptyset$ by (iv), $C_{m}$ and $C_{k}$ being sets as elements of $X$.