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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $X$ be a set, let sequences be as in Sequences (i), and let the union $\bigcup_{m\in\mathbb{N}}A_{m}$ of a sequence $(A_{m})$ be the union of the family $(A_{m})_{m\in\mathbb{N}}$, as in Sets and Maps: Ordinary Notation (vi) and Indexed Families of Sets and Their Union, Intersection and Product (ii). Intersections and disjointness are as in The Boolean Operations on Classes, Disjointness, and the Universal Class (i) and The Boolean Operations on Classes, Disjointness, and the Universal Class (ii), $\subseteq$ is as in Subclasses and Subsets (i), and $\emptyset$ is the empty set. The terms of a sequence in $X$ are sets, being elements of $X$.

(i) Let $(A_{m})$ be a sequence in $X$ with $A_{m}\subseteq A_{m+1}$ for every $m\in\mathbb{N}$. Then $A_{k}\subseteq A_{n}$ for all $k,n\in\mathbb{N}$ with $k\le n$.

(ii) Let $(A_{m})$ be a sequence in $X$ with $A_{m+1}\subseteq A_{m}$ for every $m\in\mathbb{N}$. Then $A_{n}\subseteq A_{k}$ for all $k,n\in\mathbb{N}$ with $k\le n$; in particular $A_{n}\subseteq A_{1}$ for every $n\in\mathbb{N}$.

(iii) Let $(A_{m})$ be a sequence in $X$, let $Y$ be a set, and let $(A_{m}\cap Y)$ be the sequence in the power set $\mathcal{P}(Y)$ with $m$-th term $A_{m}\cap Y$, which exists by Sequences and Maps of Sets: Complements, Traces, Two-Term Sequences, the Disjointing Sequence, and Sequences in a Subset (ii). Then $\bigcup_{m\in\mathbb{N}}(A_{m}\cap Y)=\Big(\bigcup_{m\in\mathbb{N}}A_{m}\Big)\cap Y$.

(iv) For sets $A$ and $B$: $A\cap B=\emptyset$ if and only if $A$ and $B$ are disjoint, that is, if and only if no set is an element of both $A$ and $B$.

(v) Let $(A_{m})$ and $(C_{m})$ be sequences in $X$ with $C_{m}\subseteq A_{m}$ for every $m\in\mathbb{N}$ and $A_{m}\cap A_{k}=\emptyset$ for all $m,k\in\mathbb{N}$ with $m\neq k$. Then $C_{m}\cap C_{k}=\emptyset$ for all $m,k\in\mathbb{N}$ with $m\neq k$.